Update holomorphic_primitive2.lean

Nevanlinna/holomorphic_primitive2.lean

@@ -47,22 +47,110 @@ theorem primitive_fderivAtBasepointZero
     arg 1
     arg 2
     rw [this]
-  have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
-    abel
 
-  have t₀ {r : ℝ} : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := by
+  obtain ⟨s, h₁s, h₂s⟩ : ∃ s ⊆ f⁻¹' Metric.ball (f 0) (c / (4 : ℝ)), IsOpen s ∧ 0 ∈ s := by
-    apply Continuous.intervalIntegrable
+    have B : Metric.ball (f 0) (c / 4) ∈ nhds (f 0) := by
-    apply Continuous.comp
+      apply Metric.ball_mem_nhds (f 0)
+      linarith
+    apply eventually_nhds_iff.mp
+    apply continuousAt_def.1
+    apply Continuous.continuousAt
+    fun_prop
+
+    apply continuousAt_def.1
+    apply hf.continuousAt
+    exact Metric.ball_mem_nhds 0 hR
+    apply Metric.ball_mem_nhds (f 0)
+    simpa
+
+  obtain ⟨ε, h₁ε, h₂ε⟩ : ∃ ε > 0, (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ s ∧ (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ Metric.ball 0 R := by
+    obtain ⟨ε', h₁ε', h₂ε'⟩ : ∃ ε' > 0, Metric.ball 0 ε' ⊆ s ∩ Metric.ball 0 R := by
+      apply Metric.mem_nhds_iff.mp
+      apply IsOpen.mem_nhds
+      apply IsOpen.inter
+      exact h₂s.1
+      exact Metric.isOpen_ball
+      constructor
+      · exact h₂s.2
+      · simpa
+
+    use (2 : ℝ)⁻¹ * ε'
+
+    constructor
+    · simpa
+    · constructor
+      · intro x hx
+        apply (h₂ε' _).1
+        simp
+        calc Complex.abs x
+        _ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x
+        _ < (2 : ℝ)⁻¹ * ε' + |x.im| := by
+          apply (add_lt_add_iff_right |x.im|).mpr
+          have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1
+          simp at this
+          exact this
+        _ < (2 : ℝ)⁻¹ * ε' + (2 : ℝ)⁻¹ * ε' := by
+          apply (add_lt_add_iff_left ((2 : ℝ)⁻¹ * ε')).mpr
+          have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2
+          simp at this
+          exact this
+        _ = ε' := by
+          rw [← add_mul]
+          abel_nf
+          simp
+      · intro x hx
+        apply (h₂ε' _).2
+        simp
+        calc Complex.abs x
+        _ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x
+        _ < (2 : ℝ)⁻¹ * ε' + |x.im| := by
+          apply (add_lt_add_iff_right |x.im|).mpr
+          have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1
+          simp at this
+          exact this
+        _ < (2 : ℝ)⁻¹ * ε' + (2 : ℝ)⁻¹ * ε' := by
+          apply (add_lt_add_iff_left ((2 : ℝ)⁻¹ * ε')).mpr
+          have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2
+          simp at this
+          exact this
+        _ = ε' := by
+          rw [← add_mul]
+          abel_nf
+          simp
+
+  have h₃ε : ∀ y ∈ (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε), ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by
+    intro y hy
+    apply mem_ball_iff_norm.mp
+    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 : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by
+  have t₁ {r : ℝ}  (hr : r ∈ Metric.ball 0 ε) : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by
-    apply Continuous.intervalIntegrable
+    apply ContinuousOn.intervalIntegrable
-    apply Continuous.comp
+    apply ContinuousOn.comp
-    exact hf
+    apply hf
     fun_prop
+    intro x hx
+    simpa
+
+
   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
@@ -82,6 +170,9 @@ theorem primitive_fderivAtBasepointZero
     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
@@ -89,63 +180,12 @@ theorem primitive_fderivAtBasepointZero
     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]
 
-  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
-    fun_prop
-
-    apply continuousAt_def.1
-    apply hf.continuousAt
-    exact Metric.ball_mem_nhds 0 hR
-    apply Metric.ball_mem_nhds (f 0)
-    simpa
-
-  obtain ⟨ε, h₁ε, h₂ε⟩ : ∃ ε > 0, (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ s := by
-    obtain ⟨ε', h₁ε', h₂ε'⟩ : ∃ ε' > 0, Metric.ball 0 ε' ⊆ s ∩ Metric.ball 0 R := by
-      apply Metric.mem_nhds_iff.mp
-      apply IsOpen.mem_nhds
-      apply IsOpen.inter
-      exact h₂s.1
-      exact Metric.isOpen_ball
-      constructor
-      · exact h₂s.2
-      · simpa
-    use (2 : ℝ)⁻¹ * ε'
-    constructor
-    · simpa
-    · intro x hx
-      apply Set.inter_subset_left
-      apply h₂ε'
-      simp
-      calc Complex.abs x
-      _ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x
-      _ < (2 : ℝ)⁻¹ * ε' + |x.im| := by
-        apply (add_lt_add_iff_right |x.im|).mpr
-        have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1
-        simp at this
-        exact this
-      _ < (2 : ℝ)⁻¹ * ε' + (2 : ℝ)⁻¹ * ε' := by
-        apply (add_lt_add_iff_left ((2 : ℝ)⁻¹ * ε')).mpr
-        have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2
-        simp at this
-        exact this
-      _ = ε' := by
-        rw [← add_mul]
-        abel_nf
-        simp
-
-  have h₃ε : ∀ y ∈ (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε), ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by
-    intro y hy
-    apply mem_ball_iff_norm.mp
-    exact h₁s (h₂ε hy)
 
   use Metric.ball 0 (ε / (4 : ℝ))
   constructor