Nevanlinna/holomorphic_JensenFormula.lean

@@ -1,4 +1,3 @@
-import Nevanlinna.analyticOn_zeroSet
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
 import Nevanlinna.specialFunctions_CircleIntegral_affine
@@ -6,38 +5,31 @@ import Nevanlinna.specialFunctions_CircleIntegral_affine
 
 theorem jensen_case_R_eq_one
   (f : ℂ → ℂ)
-  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
+  (h₁f : Differentiable ℂ f)
   (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 : Differentiable ℂ F)
-  (h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, F z ≠ 0)
+  (h₂F : ∀ z, F z ≠ 0)
-  (h₃F : f = fun z ↦ (F z) * ∏ s : S, (z - a s)) :
+  (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
+  have t₀ : ∀ z ∈ Metric.ball 0 2, HarmonicAt logAbsF z := by
-    intro z hz
+    intro z _
     apply logabs_of_holomorphicAt_is_harmonic
-    apply h₁F z hz
+    apply h₁F.holomorphicAt
-    exact h₂F z hz
+    exact h₂F z
 
   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 hR : (0 : ℝ) < (1 : ℝ) := by apply Real.zero_lt_one
+    have hρ : (1 : ℝ) < (2 : ℝ) := by linarith
+    apply harmonic_meanValue 2 1 hR hρ t₀
+
 
   have t₂ : ∀ s, f (a s) = 0 := by
     intro s
@@ -49,8 +41,8 @@ theorem jensen_case_R_eq_one
     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
+  have s₀ : ∀ z, f z ≠ 0 → logAbsf z = logAbsF z + ∑ s, Real.log ‖z - a s‖ := by
-    intro z h₁z h₂z
+    intro z hz
     dsimp [logAbsf]
     rw [h₃F]
     simp_rw [Complex.abs.map_mul]
@@ -61,34 +53,31 @@ theorem jensen_case_R_eq_one
     intro s hs
     simp
     by_contra ha'
-    rw [ha'] at h₂z
+    rw [ha'] at hz
-    exact h₂z (t₂ s)
+    exact hz (t₂ s)
     -- Complex.abs (F z) ≠ 0
     simp
-    exact h₂F z h₁z
+    exact h₂F 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
+    rw [h''] at hz
     let A := t₂ s
-    exact h₂z A
+    exact hz A
 
-  have s₁ : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
+  have s₁ : ∀ z, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
-    intro z h₁z h₂z
+    intro z hz
-    rw [s₀ z h₁z]
+    rw [s₀ z hz]
     simp
-    assumption
 
-  have : 0 ∈ Metric.closedBall (0 : ℂ) 1 := by simp
+  rw [s₁ 0 h₂f] at t₁
-  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)
-      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
@@ -99,8 +88,7 @@ theorem jensen_case_R_eq_one
       rw [← this] at A
       simp at A
 
-  have {θ} : (circleMap 0 1 θ) ∈ Metric.closedBall (0 : ℂ) 1 := by simp
+  simp_rw [s₁ (circleMap 0 1 _) h₀] at t₁
-  simp_rw [s₁ (circleMap 0 1 _) this h₀] at t₁
   rw [intervalIntegral.integral_sub] at t₁
   rw [intervalIntegral.integral_finset_sum] at t₁
 
@@ -145,10 +133,7 @@ theorem jensen_case_R_eq_one
   apply ContinuousAt.comp
   apply Complex.continuous_abs.continuousAt
   apply ContinuousAt.comp
-  apply ContDiffAt.continuousAt (f := f) (𝕜 := ℝ) (n := 1)
+  apply h₁f.continuous.continuousAt
-  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)

Nevanlinna/holomorphic_JensenFormula2.lean

@@ -1,163 +1,41 @@
 import Mathlib.Analysis.Complex.CauchyIntegral
-import Mathlib.Analysis.Analytic.IsolatedZeros
-import Nevanlinna.analyticOn_zeroSet
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
-
+import Mathlib.Analysis.Analytic.IsolatedZeros
-open Real
 
 
-def ZeroFinset
+lemma xx
   {f : ℂ → ℂ}
-  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z) :
+  {S : Set ℂ}
-  Finset ℂ := by
+  (h₁S : IsPreconnected S)
+  (h₂S : IsCompact S)
+  (hf : ∀ s ∈ S, AnalyticAt ℂ f s) :
+  ∃ o : ℂ → ℕ, ∃ F : ℂ → ℂ, ∀ z ∈ S, (AnalyticAt ℂ F z) ∧ (F z ≠ 0) ∧ (f z = F z * ∏ᶠ s ∈ S, (z - s) ^ (o s)) := by
 
-  let Z := f⁻¹' {0} ∩ Metric.closedBall (0 : ℂ) 1
+  let o : ℂ → ℕ := by
-  have hZ : Set.Finite Z := by sorry
+    intro z
-  exact hZ.toFinset
+    if hz : z ∈ S then
+      let A := hf z hz
+      let B := A.order
 
+      exact (A.order : ⊤)
+    else
+      exact 0
 
-def order
-  {f : ℂ → ℂ}
-  {hf : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z} :
-  ZeroFinset hf → ℕ := by sorry
-
-
-lemma ZeroFinset_mem_iff
-  {f : ℂ → ℂ}
-  (hf : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
-  (z : ℂ) :
-  z ∈ ↑(ZeroFinset hf) ↔ z ∈ Metric.closedBall 0 1 ∧ f z = 0 := by
   sorry
 
 
-theorem jensen_case_R_eq_one
+theorem jensen_case_R_eq_one'
   (f : ℂ → ℂ)
-  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
+  (h₁f : Differentiable ℂ f)
-  (h'₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, AnalyticAt ℂ f z)
+  (h₂f : f 0 ≠ 0)
-  (h₂f : f 0 ≠ 0) :
+  (S : Finset ℕ)
-  log ‖f 0‖ = -∑ s : ZeroFinset h₁f, order s * log (‖s.1‖⁻¹) + (2 * π )⁻¹ * ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ := by
+  (a : S → ℂ)
-
+  (ha : ∀ s, a s ∈ Metric.ball 0 1)
-  have F : ℂ → ℂ := by sorry
+  (F : ℂ → ℂ)
-  have h₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by sorry
+  (h₁F : Differentiable ℂ F)
-  have h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, F z ≠ 0 := by sorry
+  (h₂F : ∀ z, F z ≠ 0)
-  have h₃F : f = fun z ↦ (F z) * ∏ s : ZeroFinset h₁f, (z - s) ^ (order s) := by sorry
+  (h₃F : f = fun z ↦ (F z) * ∏ s : S, (z - a s))
-
+  :
-  let G := fun z ↦ log ‖F z‖ + ∑ s : ZeroFinset h₁f, (order s) * log ‖z - 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 decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
-    intro z h₁z h₂z
-
-    conv =>
-      left
-      arg 1
-      rw [h₃F]
-      rw [norm_mul]
-      rw [norm_prod]
-      right
-      arg 2
-      intro b
-      rw [norm_pow]
-    simp only [Complex.norm_eq_abs, Finset.univ_eq_attach]
-    rw [Real.log_mul]
-    rw [Real.log_prod]
-    conv =>
-      left
-      right
-      arg 2
-      intro s
-      rw [Real.log_pow]
-    dsimp [G]
-
-    -- ∀ x ∈ (ZeroFinset h₁f).attach, Complex.abs (z - ↑x) ^ order x ≠ 0
-    simp
-    intro s hs
-    rw [ZeroFinset_mem_iff h₁f s] at hs
-    rw [← hs.2] at h₂z
-    tauto
-
-    -- Complex.abs (F z) ≠ 0
-    simp
-    exact h₂F z h₁z
-
-    -- ∏ I : { x // x ∈ S }, Complex.abs (z - a I) ≠ 0
-    by_contra C
-    obtain ⟨s, h₁s, h₂s⟩ := Finset.prod_eq_zero_iff.1 C
-    simp at h₂s
-    rw [← ((ZeroFinset_mem_iff h₁f s).1 (Finset.coe_mem s)).2, h₂s.1] at h₂z
-    tauto
-
-  have : ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ = ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) := by
-    rw [intervalIntegral.integral_congr_ae]
-    rw [MeasureTheory.ae_iff]
-    apply Set.Countable.measure_zero
-    simp
-
-    have t₀ : {a | a ∈ Ι 0 (2 * π) ∧ ¬log ‖f (circleMap 0 1 a)‖ = G (circleMap 0 1 a)}
-      ⊆ (circleMap 0 1)⁻¹' (Metric.closedBall 0 1 ∩ f⁻¹' {0}) := by
-      intro a ha
-      simp at ha
-      simp
-      by_contra C
-      have : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 := by
-        sorry
-      exact ha.2 (decompose_f (circleMap 0 1 a) this C)
-
-    apply Set.Countable.mono t₀
-    apply Set.Countable.preimage_circleMap
-    apply Set.Finite.countable
-    apply finiteZeros
-
-    -- IsPreconnected (Metric.closedBall (0 : ℂ) 1)
-    apply IsConnected.isPreconnected
-    apply Convex.isConnected
-    exact convex_closedBall 0 1
-    exact Set.nonempty_of_nonempty_subtype
-    --
-    exact isCompact_closedBall 0 1
-    --
-    exact h'₁f
-    use 0
-    exact ⟨Metric.mem_closedBall_self (zero_le_one' ℝ), h₂f⟩
-    exact Ne.symm (zero_ne_one' ℝ)
-
-  have h₁Gi : ∀ i ∈ (ZeroFinset h₁f).attach, IntervalIntegrable (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π) := by
-    -- This is hard. Need to invoke specialFunctions_CircleIntegral_affine.
-    sorry
-
-  have : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x)))) + ∑ x ∈ (ZeroFinset h₁f).attach, ↑(order x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
-    dsimp [G]
-    rw [intervalIntegral.integral_add]
-    rw [intervalIntegral.integral_finset_sum]
-    simp_rw [intervalIntegral.integral_const_mul]
-
-    --  ∀ i ∈ (ZeroFinset h₁f).attach, IntervalIntegrable (fun x => ↑(order i) *
-    --  log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π)
-
-    -- This won't work, because the function **is not** continuous. Need to fix.
-    intro i hi
-    apply IntervalIntegrable.const_mul
-    exact h₁Gi i hi
-
-    apply Continuous.intervalIntegrable
-    apply continuous_iff_continuousAt.2
-    intro x
-    have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑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
-
-    sorry
-
-
   sorry