From 93006a2a7e9c318b9684997d9f2c822a6c1b253c Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 20 Dec 2024 09:42:56 +0100
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/firstMain.lean                     |  13 +-
 .../stronglyMeromorphic_JensenFormula.lean    | 115 +++++++++++-------
 2 files changed, 80 insertions(+), 48 deletions(-)

diff --git a/Nevanlinna/firstMain.lean b/Nevanlinna/firstMain.lean
index a441d8f..10d86df 100644
--- a/Nevanlinna/firstMain.lean
+++ b/Nevanlinna/firstMain.lean
@@ -1,8 +1,9 @@
 import Mathlib.MeasureTheory.Integral.CircleIntegral
 import Nevanlinna.divisor
-import Nevanlinna.stronglyMeromorphicOn
 import Nevanlinna.meromorphicOn_divisor
 import Nevanlinna.meromorphicOn_integrability
+import Nevanlinna.stronglyMeromorphicOn
+import Nevanlinna.stronglyMeromorphic_JensenFormula
 
 open Real
 
@@ -158,20 +159,20 @@ theorem Nevanlinna_firstMain₁
   rw [add_eq_of_eq_sub]
   unfold MeromorphicOn.T_infty
 
-  have {A B C D : ℝ → ℝ} : A + B - (C + D) = A - C + (B - D) := by
+  have {A B C D : ℝ → ℝ} : A + B - (C + D) = A - C - (D - B) := by
     ring
   rw [this]
   clear this
 
+  rw [Nevanlinna_counting₀ h₁f]
+  rw [Nevanlinna_counting h₁f]
   funext r
   simp
   rw [← Nevanlinna_proximity h₁f]
 
+  have hr : 0 < r := by sorry
 
-
-  unfold MeromorphicOn.N_infty
-  unfold MeromorphicOn.m_infty
-  simp
+  let A := jensen
   sorry
 
 theorem Nevanlinna_firstMain₂
diff --git a/Nevanlinna/stronglyMeromorphic_JensenFormula.lean b/Nevanlinna/stronglyMeromorphic_JensenFormula.lean
index 9d4c52e..ee21ca5 100644
--- a/Nevanlinna/stronglyMeromorphic_JensenFormula.lean
+++ b/Nevanlinna/stronglyMeromorphic_JensenFormula.lean
@@ -3,50 +3,11 @@ import Nevanlinna.stronglyMeromorphicOn_eliminate
 
 open Real
 
-lemma jensen₀
-  {R : ℝ}
-  (hR : 0 < R)
-  (f : ℂ → ℂ)
-  (h₁f : StronglyMeromorphicOn f (Metric.closedBall 0 R))
-  (h₂f : f 0 ≠ 0) :
-  ∃ F : ℂ → ℂ,
-    AnalyticOnNhd ℂ F (Metric.closedBall (0 : ℂ) R)
-    ∧ (∀ (u : (Metric.closedBall (0 : ℂ) R)), F u ≠ 0)
-    ∧ (fun z ↦ log ‖f z‖) =ᶠ[Filter.codiscreteWithin (Metric.closedBall (0 : ℂ) R)] (fun z ↦ log ‖F z‖ + ∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log ‖z - s‖) := by
-
-  have h₁U : IsConnected (Metric.closedBall (0 : ℂ) R) := by
-    constructor
-    · apply Metric.nonempty_closedBall.mpr
-      exact le_of_lt hR
-    · exact (convex_closedBall (0 : ℂ) R).isPreconnected
-
-  have h₂U : IsCompact (Metric.closedBall (0 : ℂ) R) := isCompact_closedBall (0 : ℂ) R
-
-
-  obtain ⟨F, h₁F, h₂F, h₃F, h₄F⟩ := MeromorphicOn.decompose₃' h₂U h₁U h₁f (by use ⟨0, Metric.mem_closedBall_self (le_of_lt hR)⟩)
-
-  use F
-  constructor
-  · exact h₂F
-  · constructor
-    · exact fun u ↦ h₃F u
-    · rw [Filter.eventuallyEq_iff_exists_mem]
-      use {z | f z ≠ 0}
-      constructor
-      · sorry
-      · intro z hz
-        simp at hz
-        nth_rw 1 [h₄F]
-        simp only [Pi.mul_apply, norm_mul]
-
-
-        sorry
-
-
-theorem jensen
+theorem jensen₀
   {R : ℝ}
   (hR : 0 < R)
   (f : ℂ → ℂ)
+  -- WARNING: Not needed. MeromorphicOn suffices
   (h₁f : StronglyMeromorphicOn f (Metric.closedBall 0 R))
   (h₂f : f 0 ≠ 0) :
   log ‖f 0‖ = -∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log (R * ‖s‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by
@@ -183,7 +144,7 @@ theorem jensen
         rcases C with C₁|C₂
         · assumption
         · let B := h₁f.meromorphicOn.order_ne_top' h₁U
-          let C := fun q ↦ B q ⟨(circleMap 0 R a), t₀⟩
+          let C := fun q ↦ B.1 q ⟨(circleMap 0 R a), t₀⟩
           rw [C₂] at C
           have : ∃ u : (Metric.closedBall (0 : ℂ) R), (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
             use ⟨(0 : ℂ), (by simp; exact le_of_lt hR)⟩
@@ -440,3 +401,73 @@ theorem jensen
   rw [hCon] at hs
   simp at hs
   exact hs h'''₂f
+
+
+theorem jensen
+  {R : ℝ}
+  (hR : 0 < R)
+  (f : ℂ → ℂ)
+  (h₁f : MeromorphicOn f (Metric.closedBall 0 R))
+  (h₁f' : StronglyMeromorphicAt f 0)
+  (h₂f : f 0 ≠ 0) :
+  log ‖f 0‖ = -∑ᶠ s, (h₁f.divisor s) * log (R * ‖s‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by
+
+  let F := h₁f.makeStronglyMeromorphicOn
+
+  have : F 0 = f 0 := by
+    unfold F
+    have : 0 ∈ (Metric.closedBall 0 R) := by
+      simp [hR]
+      exact le_of_lt hR
+    unfold MeromorphicOn.makeStronglyMeromorphicOn
+    simp [this]
+    intro h₁R
+
+    let A := StronglyMeromorphicAt.makeStronglyMeromorphic_id h₁f'
+    simp_rw [A]
+  rw [← this]
+  rw [← this] at h₂f
+  clear this
+
+  have h₁F := stronglyMeromorphicOn_of_makeStronglyMeromorphicOn h₁f
+
+  rw [jensen₀ hR F h₁F h₂f]
+
+  rw [h₁f.divisor_of_makeStronglyMeromorphicOn]
+  congr 2
+  have {x : ℝ} : log ‖F (circleMap 0 R x)‖ = (fun z ↦ log ‖F z‖) (circleMap 0 R x) := by
+    rfl
+  conv =>
+    left
+    arg 1
+    intro x
+    rw [this]
+  have {x : ℝ} : log ‖f (circleMap 0 R x)‖ = (fun z ↦ log ‖f z‖) (circleMap 0 R x) := by
+    rfl
+  conv =>
+    right
+    arg 1
+    intro x
+    rw [this]
+
+  have h'R : R ≠ 0 := by exact Ne.symm (ne_of_lt hR)
+  have hU : Metric.sphere (0 : ℂ) |R| ⊆ (Metric.closedBall (0 : ℂ) R) := by
+    have : R = |R| := by exact Eq.symm (abs_of_pos hR)
+    nth_rw 2 [this]
+    exact Metric.sphere_subset_closedBall
+
+  let A := integral_congr_changeDiscrete h'R hU (f₁ := fun z ↦ log ‖F z‖) (f₂ := fun z ↦ log ‖f z‖)
+  apply A
+  clear A
+
+  rw [Filter.eventuallyEq_iff_exists_mem]
+  have A := makeStronglyMeromorphicOn_changeDiscrete'' h₁f
+  rw [Filter.eventuallyEq_iff_exists_mem] at A
+  obtain ⟨s, h₁s, h₂s⟩ := A
+  use s
+  constructor
+  · exact h₁s
+  · intro x hx
+    let A := h₂s hx
+    simp
+    rw [A]