From ce3b3d8bd1a283011a6e6d62d99cd45b06d90102 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 3 Jan 2025 16:48: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 | 54 +++++++++++++++++++++++++++++----------
 1 file changed, 41 insertions(+), 13 deletions(-)

diff --git a/Nevanlinna/firstMain.lean b/Nevanlinna/firstMain.lean
index bca1403..a7eb92c 100644
--- a/Nevanlinna/firstMain.lean
+++ b/Nevanlinna/firstMain.lean
@@ -377,27 +377,32 @@ theorem Nevanlinna_firstMain₂
       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
+  have s₀ : ‖∫ (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
+  simp only [norm_eq_abs, sub_zero] at s₀
   rw [abs_mul]
 
+  have s₁ : |(2 * π)⁻¹| * |∫ (x : ℝ) in (0)..(2 * π), log⁺ ‖f (circleMap 0 r x)‖ - log⁺ ‖g (circleMap 0 r x)‖| ≤ |(2 * π)⁻¹| * ((log⁺ ‖a‖ + log 2) * |2 * π|) := by
+    apply mul_le_mul_of_nonneg_left
+    exact s₀
+    apply abs_nonneg
+  have : |(2 * π)⁻¹| * ((log⁺ ‖a‖ + log 2) * |2 * π|) = log⁺ ‖a‖ + log 2 := by
+    rw [mul_comm, mul_assoc]
+    have : |2 * π| * |(2 * π)⁻¹| = 1 := by
+      rw [abs_mul, abs_inv, abs_mul]
+      rw [abs_of_pos pi_pos]
+      simp [pi_ne_zero]
+      ring_nf
+      simp [pi_ne_zero]
+    rw [this]
+    simp
+  rw [this] at s₁
+  assumption
 
-  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
   --
@@ -405,3 +410,26 @@ theorem Nevanlinna_firstMain₂
   apply MeromorphicOn.sub
   exact fun x a => h₁f x trivial
   apply MeromorphicOn.const a
+
+
+open Asymptotics
+
+
+theorem Nevanlinna_firstMain'₂
+  {f : ℂ → ℂ}
+  {a : ℂ}
+  (h₁f : MeromorphicOn f ⊤) :
+  |(h₁f.T_infty) - ((h₁f.sub (MeromorphicOn.const a)).T_infty)| =O[Filter.atTop] (1 : ℝ → ℝ) := by
+
+  rw [Asymptotics.isBigO_iff']
+  use logpos ‖a‖ + log 2
+  constructor
+  · apply add_pos_of_nonneg_of_pos
+    apply logpos_nonneg
+    apply log_pos one_lt_two
+  · rw [Filter.eventually_atTop]
+    use 0
+    intro b hb
+    simp only [Pi.abs_apply, Pi.sub_apply, norm_eq_abs, abs_abs, Pi.one_apply,
+      norm_one, mul_one]
+    apply Nevanlinna_firstMain₂