From acb1f34879e5173a911a12393d91b53ea89f8d55 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 8 Aug 2024 09:55:56 +0200
Subject: [PATCH] Update holomorphic_primitive2.lean

---
 Nevanlinna/holomorphic_primitive2.lean | 153 +++++++++++++++----------
 1 file changed, 91 insertions(+), 62 deletions(-)

diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean
index 8a8ff39..61ee4b3 100644
--- a/Nevanlinna/holomorphic_primitive2.lean
+++ b/Nevanlinna/holomorphic_primitive2.lean
@@ -49,9 +49,6 @@ theorem primitive_fderivAtBasepointZero
     rw [this]
 
   obtain ⟨s, h₁s, h₂s⟩ : ∃ s ⊆ f⁻¹' Metric.ball (f 0) (c / (4 : ℝ)), IsOpen s ∧ 0 ∈ s := by
-    have B : Metric.ball (f 0) (c / 4) ∈ nhds (f 0) := by
-      apply Metric.ball_mem_nhds (f 0)
-      linarith
     apply eventually_nhds_iff.mp
     apply continuousAt_def.1
     apply Continuous.continuousAt
@@ -124,74 +121,106 @@ theorem primitive_fderivAtBasepointZero
     apply h₁s
     exact h₂ε.1 hy
 
-  have t₀ {r : ℝ} (hr : r ∈ Metric.ball 0 ε) : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := by
-    apply ContinuousOn.intervalIntegrable
-    apply ContinuousOn.comp
-    exact hf
-    have : (fun x => ({ re := x, im := 0 } : ℂ)) = Complex.ofRealLI := by rfl
-    rw [this]
-    apply Continuous.continuousOn
-    continuity
-    intro x hx
-    apply h₂ε.2
-    simp
-    constructor
-    · simp
-      calc |x|
-      _ < ε := by
-        sorry
-    · simpa
 
-  have t₁ {r : ℝ}  (hr : r ∈ Metric.ball 0 ε) : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by
-    apply ContinuousOn.intervalIntegrable
-    apply ContinuousOn.comp
-    apply hf
-    fun_prop
-    intro x hx
-    simpa
+  have intervalComputation_uIcc {x' y' : ℝ} (h : x' ∈ Set.uIcc 0 y') : |x'| ≤ |y'| := by
+    let A := h.1
+    let B := h.2
+    rcases le_total 0 y' with hy | hy
+    · simp [hy] at A
+      simp [hy] at B
+      rwa [abs_of_nonneg A, abs_of_nonneg hy]
+    · simp [hy] at A
+      simp [hy] at B
+      rw [abs_of_nonpos hy]
+      rw [abs_of_nonpos]
+      linarith [h.1]
+      exact B
 
 
-  have t₂ {a b : ℝ} : IntervalIntegrable (fun x_1 => f { re := a, im := x_1 }) MeasureTheory.volume 0 b := by
-    apply Continuous.intervalIntegrable
-    apply Continuous.comp hf
-    have : (Complex.mk a) = (fun x => Complex.I • Complex.ofRealCLM x + { re := a, im := 0 }) := by
-      funext x
-      apply Complex.ext
-      rw [Complex.add_re]
-      simp
-      simp
-    rw [this]
-    apply Continuous.add
-    continuity
-    fun_prop
-
-  have t₃ {a : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 a := by
-    apply Continuous.intervalIntegrable
-    apply Continuous.comp
-    exact hf
-    fun_prop
-
-  have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
-    abel
-  conv =>
-    left
-    intro x
-    left
-    arg 1
-    rw [this]
-    rw [← smul_sub]
-
-    rw [← intervalIntegral.integral_sub t₀ t₁]
-    rw [← intervalIntegral.integral_sub t₂ t₃]
-
   rw [Filter.eventually_iff_exists_mem]
-
-
   use Metric.ball 0 (ε / (4 : ℝ))
+
   constructor
   · apply Metric.ball_mem_nhds 0
     linarith
   · intro y hy
+
+    have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
+      abel
+    rw [this]
+    rw [← smul_sub]
+
+
+    have t₀ : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 y.re := by
+      apply ContinuousOn.intervalIntegrable
+      apply ContinuousOn.comp
+      exact hf
+      have : (fun x => ({ re := x, im := 0 } : ℂ)) = Complex.ofRealLI := by rfl
+      rw [this]
+      apply Continuous.continuousOn
+      continuity
+      intro x hx
+      apply h₂ε.2
+      simp
+      constructor
+      · simp
+        calc |x|
+        _ ≤ |y.re| := by apply intervalComputation_uIcc hx
+        _ ≤ Complex.abs y := by exact Complex.abs_re_le_abs y
+        _ < ε / 4 := by simp at hy; assumption
+        _ < ε := by linarith
+      · simpa
+    have t₁ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.re := by
+      apply ContinuousOn.intervalIntegrable
+      apply ContinuousOn.comp
+      apply hf
+      fun_prop
+      intro x _
+      simpa
+    rw [← intervalIntegral.integral_sub t₀ t₁]
+
+    have t₂ : IntervalIntegrable (fun x_1 => f { re := y.re, im := x_1 }) MeasureTheory.volume 0 y.im := by
+      apply ContinuousOn.intervalIntegrable
+      apply ContinuousOn.comp
+      exact hf
+      have : (Complex.mk y.re) = (fun x => Complex.I • Complex.ofRealCLM x + { re := y.re, im := 0 }) := by
+        funext x
+        apply Complex.ext
+        rw [Complex.add_re]
+        simp
+        simp
+      rw [this]
+      apply ContinuousOn.add
+      apply Continuous.continuousOn
+      continuity
+      fun_prop
+      intro x hx
+      apply h₂ε.2
+      constructor
+      · simp
+        calc |y.re|
+        _ ≤ Complex.abs y := by exact Complex.abs_re_le_abs y
+        _ < ε / 4 := by simp at hy; assumption
+        _ < ε := by linarith
+      · simp
+        calc |x|
+        _ ≤ |y.im| := by apply intervalComputation_uIcc hx
+        _ ≤ Complex.abs y := by exact Complex.abs_im_le_abs y
+        _ < ε / 4 := by simp at hy; assumption
+        _ < ε := by linarith
+    have t₃ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.im := by
+      apply ContinuousOn.intervalIntegrable
+      apply ContinuousOn.comp
+      exact hf
+      fun_prop
+      intro x _
+      apply h₂ε.2
+      simp
+      constructor
+      · simpa
+      · simpa
+    rw [← intervalIntegral.integral_sub t₂ t₃]
+
     have h₁y : |y.re| < ε / 4 := by
       calc |y.re|
       _ ≤ Complex.abs y := by apply Complex.abs_re_le_abs