Working

Nevanlinna/firstMain.lean

@@ -30,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
   --
@@ -67,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 [MeromorphicOn.divisor_inv (hf.restrict |r|)] at h₁x
-  rw [hh.divisor_inv] at h₁x
   simp at h₁x
   rw [hx] at h₁x
   tauto
@@ -78,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]
@@ -92,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
@@ -154,7 +154,7 @@ 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
@@ -170,10 +170,55 @@ theorem Nevanlinna_firstMain₁
   simp
   rw [← Nevanlinna_proximity h₁f]
 
-  have hr : 0 < r := by sorry
+  by_cases h₁r : r = 0
+  rw [h₁r]
+  simp
+  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]
 
-  let A := jensen
-  sorry
 
 theorem Nevanlinna_firstMain₂
   {f : ℂ → ℂ}
@@ -181,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

@@ -96,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
@@ -112,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
@@ -198,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
+    apply intervalIntegrable_logAbs_circleMap_sub_const
-    by_cases h₂i : ‖i‖ = R
+    linarith
-    -- case pos
+    --
-    sorry
-    --exact int'₂ h₂i
     -- 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
-
+    let A := h₃F ⟨(circleMap 0 R x), circleMap_mem_closedBall 0 (le_of_lt hR) x⟩
-    by_contra ha'
+    exact A
-    conv at h₂i =>
-      arg 1
-      rw [← ha']
-      rw [Complex.norm_eq_abs]
-      rw [abs_circleMap_zero R x]
-      simp
-    linarith
     --
     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
+    let A := h₂F (circleMap 0 R x) (circleMap_mem_closedBall 0 (le_of_lt hR) x)
-    simp
+    apply A.continuousAt
-    have : (circleMap 0 R x) ∈ (Metric.closedBall 0 R) := by
+    exact (continuous_circleMap 0 R).continuousAt
-      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
     -- 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
@@ -273,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