From fe0d8a5f5ee581e69272d4a42b9a0332d59fdb99 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 13 Sep 2024 07:42:07 +0200 Subject: [PATCH] Delete holomorphic_JensenFormula.lean --- Nevanlinna/holomorphic_JensenFormula.lean | 172 ---------------------- 1 file changed, 172 deletions(-) delete mode 100644 Nevanlinna/holomorphic_JensenFormula.lean diff --git a/Nevanlinna/holomorphic_JensenFormula.lean b/Nevanlinna/holomorphic_JensenFormula.lean deleted file mode 100644 index 96b36a0..0000000 --- a/Nevanlinna/holomorphic_JensenFormula.lean +++ /dev/null @@ -1,172 +0,0 @@ -import Nevanlinna.analyticOn_zeroSet -import Nevanlinna.harmonicAt_examples -import Nevanlinna.harmonicAt_meanValue -import Nevanlinna.specialFunctions_CircleIntegral_affine - - -theorem jensen_case_R_eq_one - (f : ℂ → ℂ) - (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z) - (h₂f : f 0 ≠ 0) - (S : Finset ℕ) - (a : S → ℂ) - (ha : ∀ s, a s ∈ Metric.ball 0 1) - (F : ℂ → ℂ) - (h₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z) - (h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, F z ≠ 0) - (h₃F : f = fun z ↦ (F z) * ∏ s : S, (z - a s)) : - Real.log ‖f 0‖ = -∑ s, Real.log (‖a s‖⁻¹) + (2 * Real.pi)⁻¹ * ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖f (circleMap 0 1 x)‖ := by - - have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) := by sorry - have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) := by sorry - have h₁f : AnalyticOn ℂ f (Metric.closedBall (0 : ℂ) 1) := by sorry - have h₂f : ∃ u ∈ (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by sorry - - let α := AnalyticOnCompact.eliminateZeros h₁U h₂U h₁f h₂f - obtain ⟨g, A, h'₁g, h₂g, h₃g⟩ := α - have h₁g : ∀ z ∈ Metric.closedBall 0 1, HolomorphicAt F z := by sorry - - - - let logAbsF := fun w ↦ Real.log ‖F w‖ - - have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by - intro z hz - apply logabs_of_holomorphicAt_is_harmonic - apply h₁F z hz - exact h₂F z hz - - have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, logAbsF (circleMap 0 1 x)) = 2 * Real.pi * logAbsF 0 := by - apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀ - - have t₂ : ∀ s, f (a s) = 0 := by - intro s - rw [h₃F] - simp - right - apply Finset.prod_eq_zero_iff.2 - use s - simp - - let logAbsf := fun w ↦ Real.log ‖f w‖ - have s₀ : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → logAbsf z = logAbsF z + ∑ s, Real.log ‖z - a s‖ := by - intro z h₁z h₂z - dsimp [logAbsf] - rw [h₃F] - simp_rw [Complex.abs.map_mul] - rw [Complex.abs_prod] - rw [Real.log_mul] - rw [Real.log_prod] - rfl - intro s hs - simp - by_contra ha' - rw [ha'] at h₂z - exact h₂z (t₂ s) - -- Complex.abs (F z) ≠ 0 - simp - exact h₂F z h₁z - -- ∏ I : { x // x ∈ S }, Complex.abs (z - a I) ≠ 0 - by_contra h' - obtain ⟨s, h's, h''⟩ := Finset.prod_eq_zero_iff.1 h' - simp at h'' - rw [h''] at h₂z - let A := t₂ s - exact h₂z A - - have s₁ : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by - intro z h₁z h₂z - rw [s₀ z h₁z] - simp - assumption - - have : 0 ∈ Metric.closedBall (0 : ℂ) 1 := by simp - rw [s₁ 0 this h₂f] at t₁ - - have h₀ {x : ℝ} : f (circleMap 0 1 x) ≠ 0 := by - rw [h₃F] - simp - constructor - · have : (circleMap 0 1 x) ∈ Metric.closedBall (0 : ℂ) 1 := by simp - exact h₂F (circleMap 0 1 x) this - · by_contra h' - obtain ⟨s, _, h₂s⟩ := Finset.prod_eq_zero_iff.1 h' - have : circleMap 0 1 x = a s := by - rw [← sub_zero (circleMap 0 1 x)] - nth_rw 2 [← h₂s] - simp - let A := ha s - rw [← this] at A - simp at A - - have {θ} : (circleMap 0 1 θ) ∈ Metric.closedBall (0 : ℂ) 1 := by simp - simp_rw [s₁ (circleMap 0 1 _) this h₀] at t₁ - rw [intervalIntegral.integral_sub] at t₁ - rw [intervalIntegral.integral_finset_sum] at t₁ - - simp_rw [int₀ (ha _)] at t₁ - simp at t₁ - rw [t₁] - simp - have {w : ℝ} : Real.pi⁻¹ * 2⁻¹ * (2 * Real.pi * w) = w := by - ring_nf - simp [mul_inv_cancel₀ Real.pi_ne_zero] - rw [this] - simp - rfl - -- ∀ i ∈ Finset.univ, IntervalIntegrable (fun x => Real.log ‖circleMap 0 1 x - a i‖) MeasureTheory.volume 0 (2 * Real.pi) - intro i _ - apply Continuous.intervalIntegrable - apply continuous_iff_continuousAt.2 - intro x - have : (fun x => Real.log ‖circleMap 0 1 x - a i‖) = Real.log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - a i) := - rfl - rw [this] - apply ContinuousAt.comp - apply Real.continuousAt_log - simp - by_contra ha' - let A := ha i - rw [← ha'] at A - simp at A - apply ContinuousAt.comp - apply Complex.continuous_abs.continuousAt - fun_prop - -- IntervalIntegrable (fun x => logAbsf (circleMap 0 1 x)) MeasureTheory.volume 0 (2 * Real.pi) - apply Continuous.intervalIntegrable - apply continuous_iff_continuousAt.2 - intro x - have : (fun x => logAbsf (circleMap 0 1 x)) = Real.log ∘ Complex.abs ∘ f ∘ (fun x ↦ circleMap 0 1 x) := - rfl - rw [this] - apply ContinuousAt.comp - simp - exact h₀ - apply ContinuousAt.comp - apply Complex.continuous_abs.continuousAt - apply ContinuousAt.comp - apply ContDiffAt.continuousAt (f := f) (𝕜 := ℝ) (n := 1) - apply HolomorphicAt.contDiffAt - apply h₁f - simp - let A := continuous_circleMap 0 1 - apply A.continuousAt - -- IntervalIntegrable (fun x => ∑ s : { x // x ∈ S }, Real.log ‖circleMap 0 1 x - a s‖) MeasureTheory.volume 0 (2 * Real.pi) - apply Continuous.intervalIntegrable - apply continuous_finset_sum - intro i _ - apply continuous_iff_continuousAt.2 - intro x - have : (fun x => Real.log ‖circleMap 0 1 x - a i‖) = Real.log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - a i) := - rfl - rw [this] - apply ContinuousAt.comp - apply Real.continuousAt_log - simp - by_contra ha' - let A := ha i - rw [← ha'] at A - simp at A - apply ContinuousAt.comp - apply Complex.continuous_abs.continuousAt - fun_prop