From 567b08aa5b458c37abdd33b9971a29f7604478c6 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 21 Aug 2024 17:04:45 +0200
Subject: [PATCH] =?UTF-8?q?working=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Nevanlinna/holomorphic_JensenFormula.lean  |  12 ++
 Nevanlinna/holomorphic_JensenFormula2.lean | 176 +++++++++++++++++----
 2 files changed, 161 insertions(+), 27 deletions(-)

diff --git a/Nevanlinna/holomorphic_JensenFormula.lean b/Nevanlinna/holomorphic_JensenFormula.lean
index daaf606..01d6eb7 100644
--- a/Nevanlinna/holomorphic_JensenFormula.lean
+++ b/Nevanlinna/holomorphic_JensenFormula.lean
@@ -1,3 +1,4 @@
+import Nevanlinna.analyticOn_zeroSet
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
 import Nevanlinna.specialFunctions_CircleIntegral_affine
@@ -16,6 +17,17 @@ theorem jensen_case_R_eq_one
   (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
diff --git a/Nevanlinna/holomorphic_JensenFormula2.lean b/Nevanlinna/holomorphic_JensenFormula2.lean
index 1c2881a..b295282 100644
--- a/Nevanlinna/holomorphic_JensenFormula2.lean
+++ b/Nevanlinna/holomorphic_JensenFormula2.lean
@@ -1,41 +1,163 @@
 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
 
 
-lemma xx
+def ZeroFinset
   {f : ℂ → ℂ}
-  {S : Set ℂ}
-  (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
+  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z) :
+  Finset ℂ := by
 
-  let o : ℂ → ℕ := by
-    intro z
-    if hz : z ∈ S then
-      let A := hf z hz
-      let B := A.order
+  let Z := f⁻¹' {0} ∩ Metric.closedBall (0 : ℂ) 1
+  have hZ : Set.Finite Z := by sorry
+  exact hZ.toFinset
 
-      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 : Differentiable ℂ f)
-  (h₂f : f 0 ≠ 0)
-  (S : Finset ℕ)
-  (a : S → ℂ)
-  (ha : ∀ s, a s ∈ Metric.ball 0 1)
-  (F : ℂ → ℂ)
-  (h₁F : Differentiable ℂ F)
-  (h₂F : ∀ z, 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
+  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
+  (h'₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, AnalyticAt ℂ f z)
+  (h₂f : f 0 ≠ 0) :
+  log ‖f 0‖ = -∑ s : ZeroFinset h₁f, order s * log (‖s.1‖⁻¹) + (2 * π )⁻¹ * ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ := by
+
+  have F : ℂ → ℂ := by sorry
+  have h₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by sorry
+  have h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, F z ≠ 0 := by sorry
+  have h₃F : f = fun z ↦ (F z) * ∏ s : ZeroFinset h₁f, (z - s) ^ (order s) := by sorry
+
+  let G := fun z ↦ log ‖F z‖ + ∑ s : ZeroFinset h₁f, (order s) * log ‖z - s‖
+
+  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