From 08e963e801890edfcf52507ca862561a84311709 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 3 Jan 2025 14:07:53 +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 | 124 +++++++++++++++++++++++++++++++++++++-
 Nevanlinna/logpos.lean    |  32 ++++++++++
 2 files changed, 153 insertions(+), 3 deletions(-)

diff --git a/Nevanlinna/firstMain.lean b/Nevanlinna/firstMain.lean
index b4b1050..bca1403 100644
--- a/Nevanlinna/firstMain.lean
+++ b/Nevanlinna/firstMain.lean
@@ -41,8 +41,8 @@ noncomputable def MeromorphicOn.N_infty
 
 theorem Nevanlinna_counting₁₁
   {f : ℂ → ℂ}
-  {a : ℂ}
-  (hf : MeromorphicOn f ⊤) :
+  (hf : MeromorphicOn f ⊤)
+  (a : ℂ) :
   (hf.add (MeromorphicOn.const a)).N_infty = hf.N_infty := by
 
   funext r
@@ -94,6 +94,19 @@ theorem Nevanlinna_counting₁₁
   clear this
   simp [G]
 
+theorem Nevanlinna_counting'₁₁
+  {f : ℂ → ℂ}
+  (hf : MeromorphicOn f ⊤)
+  (a : ℂ) :
+  (hf.sub (MeromorphicOn.const a)).N_infty = hf.N_infty := by
+  have : (f - fun x => a) = (f + fun x => -a) := by
+    funext x
+    simp; ring
+  have : (hf.sub (MeromorphicOn.const a)).N_infty = (hf.add (MeromorphicOn.const (-a))).N_infty := by
+    simp
+  rw [this]
+  exact Nevanlinna_counting₁₁ hf (-a)
+
 
 theorem Nevanlinna_counting₀
   {f : ℂ → ℂ}
@@ -286,4 +299,109 @@ theorem Nevanlinna_firstMain₂
 
   -- See Lang, p. 168
 
-  sorry
+  have : (h₁f.T_infty r) - ((h₁f.sub (MeromorphicOn.const a)).T_infty r) = (h₁f.m_infty r) - ((h₁f.sub (MeromorphicOn.const a)).m_infty r) := by
+    unfold MeromorphicOn.T_infty
+    rw [Nevanlinna_counting'₁₁ h₁f a]
+    simp
+  rw [this]
+  clear this
+
+  unfold MeromorphicOn.m_infty
+  rw [←mul_sub]
+  rw [←intervalIntegral.integral_sub]
+
+  let g := f - (fun _ ↦ a)
+
+  have t₀₀ (x : ℝ) : log⁺ ‖f (circleMap 0 r x)‖ ≤ log⁺ ‖g (circleMap 0 r x)‖ + log⁺ ‖a‖ + log 2 := by
+    unfold g
+    simp only [Pi.sub_apply]
+
+    calc log⁺ ‖f (circleMap 0 r x)‖
+    _ = log⁺ ‖g (circleMap 0 r x) + a‖ := by
+      unfold g
+      simp
+    _ ≤ log⁺ (‖g (circleMap 0 r x)‖ + ‖a‖) := by
+      apply monoOn_logpos
+      refine Set.mem_Ici.mpr ?_
+      apply norm_nonneg
+      refine Set.mem_Ici.mpr ?_
+      apply add_nonneg
+      apply norm_nonneg
+      apply norm_nonneg
+      --
+      apply norm_add_le
+    _ ≤ log⁺ ‖g (circleMap 0 r x)‖ + log⁺ ‖a‖ + log 2 := by
+      apply logpos_add_le_add_logpos_add_log2
+
+  have t₁₀ (x : ℝ) : log⁺ ‖f (circleMap 0 r x)‖ - log⁺ ‖g (circleMap 0 r x)‖ ≤ log⁺ ‖a‖ + log 2 := by
+    rw [sub_le_iff_le_add]
+    nth_rw 1 [add_comm]
+    rw [←add_assoc]
+    apply t₀₀ x
+  clear t₀₀
+
+  have t₀₁ (x : ℝ) : log⁺ ‖g (circleMap 0 r x)‖ ≤ log⁺ ‖f (circleMap 0 r x)‖ + log⁺ ‖a‖ + log 2 := by
+    unfold g
+    simp only [Pi.sub_apply]
+
+    calc log⁺ ‖g (circleMap 0 r x)‖
+    _ = log⁺ ‖f (circleMap 0 r x) - a‖ := by
+      unfold g
+      simp
+    _ ≤ log⁺ (‖f (circleMap 0 r x)‖ + ‖a‖) := by
+      apply monoOn_logpos
+      refine Set.mem_Ici.mpr ?_
+      apply norm_nonneg
+      refine Set.mem_Ici.mpr ?_
+      apply add_nonneg
+      apply norm_nonneg
+      apply norm_nonneg
+      --
+      apply norm_sub_le
+    _ ≤ log⁺ ‖f (circleMap 0 r x)‖ + log⁺ ‖a‖ + log 2 := by
+      apply logpos_add_le_add_logpos_add_log2
+
+  have t₁₁ (x : ℝ) : log⁺ ‖g (circleMap 0 r x)‖ - log⁺ ‖f (circleMap 0 r x)‖ ≤ log⁺ ‖a‖ + log 2 := by
+    rw [sub_le_iff_le_add]
+    nth_rw 1 [add_comm]
+    rw [←add_assoc]
+    apply t₀₁ x
+  clear t₀₁
+
+  have t₂ {x : ℝ} : ‖log⁺ ‖f (circleMap 0 r x)‖ - log⁺ ‖g (circleMap 0 r x)‖‖ ≤ log⁺ ‖a‖ + log 2 := by
+    by_cases h : 0 ≤ log⁺ ‖f (circleMap 0 r x)‖ - log⁺ ‖g (circleMap 0 r x)‖
+    · rw [norm_of_nonneg h]
+      exact t₁₀ x
+    · rw [norm_of_nonpos (by linarith)]
+      rw [neg_sub]
+      exact t₁₁ x
+  clear t₁₀ t₁₁
+
+  have : ‖∫ (x : ℝ) in (0)..(2 * π), log⁺ ‖f (circleMap 0 r x)‖ - log⁺ ‖g (circleMap 0 r x)‖‖ ≤ (log⁺ ‖a‖ + log 2) * |2 * π - 0| := by
+    apply intervalIntegral.norm_integral_le_of_norm_le_const
+    intro x hx
+    exact t₂
+  clear t₂
+  simp only [norm_eq_abs, sub_zero] at this
+  rw [abs_mul]
+
+
+  calc |(2 * π)⁻¹| * |∫ (x : ℝ) in (0)..(2 * π), log⁺ ‖f (circleMap 0 r x)‖ - log⁺ ‖g (circleMap 0 r x)‖|
+  _ = |(2 * π)⁻¹| * ‖∫ (x : ℝ) in (0)..(2 * π), log⁺ ‖f (circleMap 0 r x)‖ - log⁺ ‖g (circleMap 0 r x)‖‖ := by
+
+    sorry
+  _ ≤ |(2 * π)⁻¹| * ((log⁺ ‖a‖ + log 2) * |2 * π|) := by
+    apply?
+
+    sorry
+  _ = log⁺ ‖a‖ + log 2 := by
+    simp [pi_ne_zero]
+  --
+
+  apply MeromorphicOn.integrable_logpos_abs_f
+  exact fun x a => h₁f x trivial
+  --
+  apply MeromorphicOn.integrable_logpos_abs_f
+  apply MeromorphicOn.sub
+  exact fun x a => h₁f x trivial
+  apply MeromorphicOn.const a
diff --git a/Nevanlinna/logpos.lean b/Nevanlinna/logpos.lean
index cd85108..2bb9875 100644
--- a/Nevanlinna/logpos.lean
+++ b/Nevanlinna/logpos.lean
@@ -35,6 +35,14 @@ theorem logpos_norm {r : ℝ} : log⁺ r = 2⁻¹ * (log r + ‖log r‖) := by
     rw [this]
     ring
 
+
+theorem logpos_nonneg
+  {x : ℝ} :
+  0 ≤ log⁺ x := by
+  unfold logpos
+  simp
+
+
 theorem logpos_abs
   {x : ℝ} :
   log⁺ x = log⁺ |x| := by
@@ -125,3 +133,27 @@ theorem logpos_add_le_add_logpos_add_log2
   · rw [add_comm a b, add_comm (log⁺ a) (log⁺ b)]
     apply logpos_add_le_add_logpos_add_log2₀
     exact le_of_not_ge h
+
+theorem monoOn_logpos :
+  MonotoneOn log⁺ (Set.Ici 0) := by
+  intro x hx y hy hxy
+  by_cases h₁x : x = 0
+  · rw [h₁x]
+    unfold logpos
+    simp
+
+  simp at hx hy
+  unfold logpos
+  simp
+  by_cases h₂x : log x ≤ 0
+  · tauto
+  · simp [h₂x]
+    simp at h₂x
+    have : log x ≤ log y := by
+      apply log_le_log
+      exact lt_of_le_of_ne hx fun a => h₁x (id (Eq.symm a))
+      assumption
+    simp [this]
+    calc 0
+    _ ≤ log x := by exact le_of_lt h₂x
+    _ ≤ log y := this