Nevanlinna/holomorphic_primitive2.lean

@@ -20,10 +20,8 @@ theorem primitive_zeroAtBasepoint
 
 theorem primitive_fderivAtBasepointZero
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  {R : ℝ}
-  (hR : 0 < R)
-  (hf : ContinuousOn f (Metric.ball 0 R)) :
+  (f : ℂ  → E)
+  (hf : ContinuousAt f 0) :
   HasDerivAt (primitive 0 f) (f 0) 0 := by
   unfold primitive
   simp
@@ -47,110 +45,20 @@ theorem primitive_fderivAtBasepointZero
     arg 1
     arg 2
     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
-    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
+  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
+    apply Continuous.intervalIntegrable
+    apply Continuous.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
+  have t₁ {r : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by
+    apply Continuous.intervalIntegrable
+    apply Continuous.comp
+    exact 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
@@ -170,9 +78,6 @@ 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
@@ -180,12 +85,22 @@ 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]
 
+  let s := f⁻¹' Metric.ball (f 0) (c / (4 : ℝ))
+  have h₁s : IsOpen s := IsOpen.preimage hf Metric.isOpen_ball
+  have h₂s : 0 ∈ s := by
+    apply Set.mem_preimage.mpr
+    apply Metric.mem_ball_self
+    linarith
+
+  obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 h₁s 0 h₂s
+
+  have h₃ε : ∀ y ∈ Metric.ball 0 ε, ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by
+    intro y hy
+    apply mem_ball_iff_norm.mp (h₂ε hy)
 
   use Metric.ball 0 (ε / (4 : ℝ))
   constructor
@@ -233,11 +148,12 @@ theorem primitive_fderivAtBasepointZero
           _ < ε / 4 := h₁y
       apply le_of_lt
       apply h₃ε { re := x, im := 0 }
-      constructor
-      · simp
-        linarith
-      · simp
-        exact h₁ε
+      rw [mem_ball_iff_norm]
+      simp
+      have : { re := x, im := 0 } = (x : ℂ) := by rfl
+      rw [this]
+      rw [Complex.abs_ofReal]
+      linarith
 
     have t₂ : ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ ≤ (c / (4 : ℝ)) * |y.im - 0| := by
       apply intervalIntegral.norm_integral_le_of_norm_le_const
@@ -250,11 +166,13 @@ theorem primitive_fderivAtBasepointZero
 
       apply le_of_lt
       apply h₃ε { re := y.re, im := x }
-      constructor
-      · simp
-        linarith
-      · simp
-        linarith
+      simp
+
+      calc Complex.abs { re := y.re, im := x }
+        _ ≤ |y.re| + |x| := by
+          apply Complex.abs_le_abs_re_add_abs_im { re := y.re, im := x }
+        _ < ε := by
+          linarith
 
     calc ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0) + Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖
       _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
@@ -335,21 +253,14 @@ theorem primitive_translation
 theorem primitive_hasDerivAtBasepoint
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   {f : ℂ  → E}
-  {R : ℝ}
   (z₀ : ℂ)
-  (hR : 0 < R)
-  (hf : ContinuousOn f (Metric.ball z₀ R)) :
+  (hf : ContinuousAt f z₀) :
   HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
 
   let g := f ∘ fun z ↦ z + z₀
-  have hg : ContinuousOn g (Metric.ball 0 R) := by
-    apply ContinuousOn.comp
-    fun_prop
-    fun_prop
-    intro x hx
-    simp
-    simp at hx
-    assumption
+  have : Continuous g := by continuity
+  let A := primitive_fderivAtBasepointZero g this
+  simp at A
 
   let B := primitive_translation g z₀ z₀
   simp at B
@@ -359,7 +270,8 @@ theorem primitive_hasDerivAtBasepoint
     simp
   rw [this] at B
   rw [B]
-  have : f z₀ = (1 : ℂ) • (f z₀) := (MulAction.one_smul (f z₀)).symm
+  have : f z₀ = (1 : ℂ) • (f z₀) := by
+    exact (MulAction.one_smul (f z₀)).symm
   conv =>
     arg 2
     rw [this]
@@ -368,7 +280,7 @@ theorem primitive_hasDerivAtBasepoint
   simp
   have : g 0 = f z₀ := by simp [g]
   rw [← this]
-  exact primitive_fderivAtBasepointZero hR hg
+  exact A
   apply HasDerivAt.sub_const
   have : (fun (x : ℂ) ↦ x) = id := by
     funext x
@@ -391,18 +303,10 @@ theorem primitive_additivity
 
   let εx := rx - dist z₀.re z₁.re
   have hεx : εx > 0 := by
-    let A := hz₁.1
-    simp at A
-    dsimp [εx]
-    rw [dist_comm]
-    simpa
+    sorry
   let εy := ry - dist z₀.im z₁.im
   have hεy : εy > 0 := by
-    let A := hz₁.2
-    simp at A
-    dsimp [εy]
-    rw [dist_comm]
-    simpa
+    sorry
 
   use εx
   use hεx
@@ -629,6 +533,7 @@ theorem primitive_additivity'
       rw [← Complex.dist_eq_re_im]; simp
       exact hz₁
     obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 lem₀Ω 0 lem₁Ω
+    have h'₁ε : 0 < ε := by exact h₁ε
 
     let ε' := (2 : ℝ)⁻¹ * ε
 
@@ -666,28 +571,20 @@ theorem primitive_additivity'
     simp
     rw [Complex.dist_eq_re_im]
 
-    have t₀ : dist x.re z₀.re < rx := Metric.mem_ball.mp hx.1
-    have t₁ : dist x.im z₀.im < ry := Metric.mem_ball.mp hx.2
-    have t₂ : √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) < √( rx ^ 2 + ry ^ 2) := by
+    have : dist x.re z₀.re < rx := Metric.mem_ball.mp hx.1
+    have : dist x.im z₀.im < ry := Metric.mem_ball.mp hx.2
+
+    have t₀ : √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) < √( rx ^ 2 + ry ^ 2) := by
       rw [Real.sqrt_lt_sqrt_iff]
       apply add_lt_add
-      · rw [sq_lt_sq]
-        dsimp [dist] at t₀
-        nth_rw 2 [abs_of_nonneg]
-        assumption
-        apply add_nonneg dist_nonneg (le_of_lt h₀ε)
-      · rw [sq_lt_sq]
-        dsimp [dist] at t₁
-        nth_rw 2 [abs_of_nonneg]
-        assumption
-        apply add_nonneg dist_nonneg (le_of_lt h₀ε)
-      apply add_nonneg
-      exact sq_nonneg (x.re - z₀.re)
-      exact sq_nonneg (x.im - z₀.im)
+      · dsimp [rx]
+
+        sorry
+      · sorry
 
     calc √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2)
     _ < √( rx ^ 2 + ry ^ 2) := by
-      exact t₂
+      exact t₀
     _ = d ε := by dsimp [d, rx, ry]
     _ < R := by exact h₁ε
 
@@ -728,29 +625,11 @@ theorem primitive_hasDerivAt
   rw [Filter.EventuallyEq.hasDerivAt_iff A]
   rw [← add_zero (f z)]
   apply HasDerivAt.add
-
-  let R' := R - dist z z₀
-  have h₀R' : 0 < R' := by
-    dsimp [R']
-    simp
-    exact hz
-  have h₁R' : Metric.ball z R' ⊆ Metric.ball z₀ R := by
-    intro x hx
-    simp
-    calc dist x z₀
-    _ ≤ dist x z + dist z z₀ := dist_triangle x z z₀
-    _ < R' + dist z z₀ := by
-      refine add_lt_add_right ?bc (dist z z₀)
-      exact hx
-    _ = R := by
-      dsimp [R']
-      simp
-
   apply primitive_hasDerivAtBasepoint
-  exact h₀R'
-  apply ContinuousOn.mono hf.continuousOn h₁R'
-  apply hasDerivAt_const
 
+  apply hf.continuousOn.continuousAt
+  apply (IsOpen.mem_nhds_iff Metric.isOpen_ball).2 hz
+  apply hasDerivAt_const
 
 
 theorem primitive_differentiable