Working

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
 
@@ -29,27 +30,28 @@ noncomputable def MeromorphicOn.N_zero
   {f : ℂ → ℂ}
   (hf : MeromorphicOn f ⊤) :
   ℝ → ℝ :=
-  fun r ↦ ∑ᶠ z, (max 0 ((hf.restrict r).divisor z)) * log (r * ‖z‖⁻¹)
+  fun r ↦ ∑ᶠ z, (max 0 ((hf.restrict |r|).divisor z)) * log (r * ‖z‖⁻¹)
 
 noncomputable def MeromorphicOn.N_infty
   {f : ℂ → ℂ}
   (hf : MeromorphicOn f ⊤) :
   ℝ → ℝ :=
-  fun r ↦ ∑ᶠ z, (max 0 (-((hf.restrict r).divisor z))) * log (r * ‖z‖⁻¹)
+  fun r ↦ ∑ᶠ z, (max 0 (-((hf.restrict |r|).divisor z))) * log (r * ‖z‖⁻¹)
 
 theorem Nevanlinna_counting₀
   {f : ℂ → ℂ}
   (hf : MeromorphicOn f ⊤) :
   hf.inv.N_infty = hf.N_zero := by
+
   funext r
   unfold MeromorphicOn.N_zero MeromorphicOn.N_infty
-  let A := (hf.restrict r).divisor.finiteSupport (isCompact_closedBall 0 r)
+  let A := (hf.restrict |r|).divisor.finiteSupport (isCompact_closedBall 0 |r|)
   repeat
     rw [finsum_eq_sum_of_support_subset (s := A.toFinset)]
   apply Finset.sum_congr rfl
   intro x hx
   congr
-  rw [hf.restrict_inv r]
+  let B := hf.restrict_inv |r|
   rw [MeromorphicOn.divisor_inv]
   simp
   --
@@ -66,9 +68,8 @@ theorem Nevanlinna_counting₀
   contrapose
   simp
   intro hx h₁x
-  rw [hf.restrict_inv r] at h₁x
-  have hh : MeromorphicOn f (Metric.closedBall 0 r) := hf.restrict r
-  rw [hh.divisor_inv] at h₁x
+
+  rw [MeromorphicOn.divisor_inv (hf.restrict |r|)] at h₁x
   simp at h₁x
   rw [hx] at h₁x
   tauto
@@ -77,13 +78,13 @@ theorem Nevanlinna_counting₀
 theorem Nevanlinna_counting
   {f : ℂ → ℂ}
   (hf : MeromorphicOn f ⊤) :
-  hf.N_zero - hf.N_infty = fun r ↦ ∑ᶠ z, ((hf.restrict r).divisor z) * log (r * ‖z‖⁻¹) := by
+  hf.N_zero - hf.N_infty = fun r ↦ ∑ᶠ z, ((hf.restrict |r|).divisor z) * log (r * ‖z‖⁻¹) := by
 
   funext r
   simp only [Pi.sub_apply]
   unfold  MeromorphicOn.N_zero MeromorphicOn.N_infty
 
-  let A := (hf.restrict r).divisor.finiteSupport (isCompact_closedBall 0 r)
+  let A := (hf.restrict |r|).divisor.finiteSupport (isCompact_closedBall 0 |r|)
   repeat
     rw [finsum_eq_sum_of_support_subset (s := A.toFinset)]
   rw [← Finset.sum_sub_distrib]
@@ -91,9 +92,9 @@ theorem Nevanlinna_counting
   congr
   funext x
   congr
-  by_cases h : 0 ≤ (hf.restrict r).divisor x
+  by_cases h : 0 ≤ (hf.restrict |r|).divisor x
   · simp [h]
-  · have h' : 0 ≤ -((hf.restrict r).divisor x) := by
+  · have h' : 0 ≤ -((hf.restrict |r|).divisor x) := by
       simp at h
       apply Int.le_neg_of_le_neg
       simp
@@ -153,26 +154,71 @@ theorem Nevanlinna_firstMain₁
   (h₁f : MeromorphicOn f ⊤)
   (h₂f : StronglyMeromorphicAt f 0)
   (h₃f : f 0 ≠ 0) :
-  (fun r ↦ log ‖f 0‖) + h₁f.inv.T_infty = h₁f.T_infty := by
+  (fun _ ↦ log ‖f 0‖) + h₁f.inv.T_infty = h₁f.T_infty := by
 
   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]
 
-
-
-  unfold MeromorphicOn.N_infty
-  unfold MeromorphicOn.m_infty
+  by_cases h₁r : r = 0
+  rw [h₁r]
   simp
-  sorry
+  have : π⁻¹ * 2⁻¹ * (2 * π * log (Complex.abs (f 0))) = (π⁻¹ * (2⁻¹ * 2) * π) * log (Complex.abs (f 0)) := by
+    ring
+  rw [this]
+  clear this
+  simp [pi_ne_zero]
+
+  by_cases hr : 0 < r
+  let A := jensen hr f (h₁f.restrict r) h₂f h₃f
+  simp at A
+  rw [A]
+  clear A
+  simp
+  have {A B : ℝ} : -A + B = B - A := by ring
+  rw [this]
+  have : |r| = r := by
+    rw [← abs_of_pos hr]
+    simp
+  rw [this]
+
+  -- case 0 < -r
+  have h₂r : 0 < -r := by
+    simp [h₁r, hr]
+    by_contra hCon
+    -- Assume ¬(r < 0), which means r >= 0
+    push_neg at hCon
+    -- Now h is r ≥ 0, so we split into cases
+    rcases lt_or_eq_of_le hCon with h|h
+    · tauto
+    · tauto
+  let A := jensen h₂r f (h₁f.restrict (-r)) h₂f h₃f
+  simp at A
+  rw [A]
+  clear A
+  simp
+  have {A B : ℝ} : -A + B = B - A := by ring
+  rw [this]
+
+  congr 1
+  congr 1
+  let A := integrabl_congr_negRadius (f := (fun z ↦ log (Complex.abs (f z)))) (r := r)
+  rw [A]
+  have : |r| = -r := by
+    rw [← abs_of_pos h₂r]
+    simp
+  rw [this]
+
 
 theorem Nevanlinna_firstMain₂
   {f : ℂ → ℂ}
@@ -180,4 +226,5 @@ theorem Nevanlinna_firstMain₂
   {r : ℝ}
   (h₁f : MeromorphicOn f ⊤) :
   |(h₁f.T_infty r) - ((h₁f.sub (MeromorphicOn.const a)).T_infty r)| ≤ logpos ‖a‖ + log 2 := by
+
   sorry

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
@@ -135,7 +96,7 @@ theorem jensen
       by_contra hCon
       rw [← hCon] at hx
       simp at hx
-      rw [← StronglyMeromorphicAt.order_eq_zero_iff] at h₂z
+      rw [← (h₁f z h₁z).order_eq_zero_iff] at h₂z
       unfold MeromorphicOn.divisor at hx
       simp [h₁z] at hx
       tauto
@@ -151,7 +112,7 @@ theorem jensen
       by_contra hCon
       rw [← hCon] at hx
       simp at hx
-      rw [← StronglyMeromorphicAt.order_eq_zero_iff] at h₂z
+      rw [← (h₁f z h₁z).order_eq_zero_iff] at h₂z
       unfold MeromorphicOn.divisor at hx
       simp [h₁z] at hx
       tauto
@@ -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)⟩
@@ -237,62 +198,28 @@ theorem jensen
     --    log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π)
     intro i _
     apply IntervalIntegrable.const_mul
-    --simp at this
-    by_cases h₂i : ‖i‖ = R
-    -- case pos
-    sorry
-    --exact int'₂ h₂i
+    apply intervalIntegrable_logAbs_circleMap_sub_const
+    linarith
+    --
     -- case neg
     apply Continuous.intervalIntegrable
     apply continuous_iff_continuousAt.2
     intro x
-    have : (fun x => log (Complex.abs (circleMap 0 R x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 R x - ↑i) :=
+    have : (fun x => log (Complex.abs ( F (circleMap 0 R x)))) = log ∘ Complex.abs ∘ F ∘ circleMap 0 R :=
       rfl
     rw [this]
     apply ContinuousAt.comp
     apply Real.continuousAt_log
     simp
-
-    by_contra ha'
-    conv at h₂i =>
-      arg 1
-      rw [← ha']
-      rw [Complex.norm_eq_abs]
-      rw [abs_circleMap_zero R x]
-      simp
-    linarith
+    let A := h₃F ⟨(circleMap 0 R x), circleMap_mem_closedBall 0 (le_of_lt hR) x⟩
+    exact A
     --
     apply ContinuousAt.comp
     apply Complex.continuous_abs.continuousAt
-    fun_prop
-    -- IntervalIntegrable (fun x => log (Complex.abs (F (circleMap 0 1 x)))) MeasureTheory.volume 0 (2 * π)
-    apply Continuous.intervalIntegrable
-    apply continuous_iff_continuousAt.2
-    intro x
-    have : (fun x => log (Complex.abs (F (circleMap 0 R x)))) = log ∘ Complex.abs ∘ F ∘ (fun x ↦ circleMap 0 R x) :=
-      rfl
-    rw [this]
     apply ContinuousAt.comp
-    apply Real.continuousAt_log
-    simp
-    have : (circleMap 0 R x) ∈ (Metric.closedBall 0 R) := by
-      simp
-      rw [abs_le]
-      simp [hR]
-      exact le_of_lt hR
-    exact h₃F ⟨(circleMap 0 R x), this⟩
-
-    -- ContinuousAt (⇑Complex.abs ∘ F ∘ fun x => circleMap 0 1 x) x
-    apply ContinuousAt.comp
-    apply Complex.continuous_abs.continuousAt
-    apply ContinuousAt.comp
-    apply DifferentiableAt.continuousAt (𝕜 := ℂ)
-    apply AnalyticAt.differentiableAt
-    apply h₂F (circleMap 0 R x)
-    simp; rw [abs_le]; simp [hR]; exact le_of_lt hR
-    -- ContinuousAt (fun x => circleMap 0 1 x) x
-    apply Continuous.continuousAt
-    apply continuous_circleMap
+    let A := h₂F (circleMap 0 R x) (circleMap_mem_closedBall 0 (le_of_lt hR) x)
+    apply A.continuousAt
+    exact (continuous_circleMap 0 R).continuousAt
     -- IntervalIntegrable (fun x => ∑ᶠ (s : ℂ), ↑(↑⋯.divisor s) * log (Complex.abs (circleMap 0 1 x - s))) MeasureTheory.volume 0 (2 * π)
     --simp? at h₁G
     have h₁G' {z : ℂ} : (Function.support fun s => (h₁f.meromorphicOn.divisor s) * log (Complex.abs (z - s))) ⊆ ↑h₃f.toFinset := by
@@ -312,9 +239,8 @@ theorem jensen
     by_cases h₂i : ‖i‖ = R
     -- case pos
     --exact int'₂ h₂i
-    sorry
+    apply intervalIntegrable_logAbs_circleMap_sub_const (Ne.symm (ne_of_lt hR))
     -- case neg
-    --have : i.1 ∈ Metric.ball (0 : ℂ) 1 := by sorry
     apply Continuous.intervalIntegrable
     apply continuous_iff_continuousAt.2
     intro x
@@ -440,3 +366,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]