working…

Nevanlinna/holomorphic_primitive2.lean

@@ -335,7 +335,6 @@ theorem primitive_additivity
   (f : ℂ  → E)
   (z₀ : ℂ)
   (rx ry : ℝ)
-  (hrx : 0 < rx)
   (hry : 0 < ry)
   (hf : DifferentiableOn ℂ f (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry))
   (z₁ : ℂ)
@@ -347,50 +346,6 @@ theorem primitive_additivity
   use ry - dist z₀.im z₁.im
   intro z hz
 
-/-
-  have H : (Set.uIcc z₁.re z.re ×ℂ Set.uIcc z₀.im z₁.im) ⊆ Metric.ball z₀ R := by
-    intro x hx
-
-    have A₁ : dist x.im z₀.im ≤ dist z₁.im z₀.im := by
-      apply Real.dist_right_le_of_mem_uIcc
-      rw [Set.uIcc_comm]
-      exact (Complex.mem_reProdIm.1 hx).2
-
-    have A₂ : dist x.re z₁.re ≤ dist z.re z₁.re := by
-      apply Real.dist_right_le_of_mem_uIcc
-      rw [Set.uIcc_comm]
-      exact (Complex.mem_reProdIm.1 hx).1
-
-    have A₃ : dist z.re z₁.re < R - dist z₁ z₀ := by
-      have : ∀ x₀ x₁ : ℂ, dist x₀.re x₁.re ≤ dist x₀ x₁ := by
-        intro x₀ x₁
-        rw [Complex.dist_eq_re_im, Real.dist_eq]
-        apply Real.le_sqrt_of_sq_le
-        simp
-        exact sq_nonneg (x₀.im - x₁.im)
-      calc dist z.re z₁.re
-        _ ≤ dist z z₁ := by apply this z z₁
-        _ < R - dist z₁ z₀ := by exact hz
-
-    simp
-
-    have B₁ : dist ⟨z₁.re, x.im⟩ z₀ ≤ dist z₁ z₀ := by
-      rw [Complex.dist_eq_re_im]
-      rw [Complex.dist_eq_re_im]
-      simp
-      apply Real.sqrt_le_sqrt
-      simp
-      exact sq_le_sq.mpr A₁
-
-    calc dist x z₀
-      _ ≤ dist x ⟨z₁.re, x.im⟩ + dist ⟨z₁.re, x.im⟩ z₀ := by apply dist_triangle
-      _ = dist x.re z₁.re + dist ⟨z₁.re, x.im⟩ z₀ := by rw [Complex.dist_of_im_eq]; rfl
-      _ ≤ dist z.re z₁.re + dist ⟨z₁.re, x.im⟩ z₀ := by apply add_le_add_right A₂
-      _ < (R - dist z₁ z₀) + dist ⟨z₁.re, x.im⟩ z₀ := by apply add_lt_add_right A₃
-      _ ≤ (R - dist z₁ z₀) + dist z₁ z₀ := by exact (add_le_add_iff_left (R - dist z₁ z₀)).mpr B₁
-      _ = R := by exact sub_add_cancel R (dist z₁ z₀)
--/
-
   unfold primitive
 
   have : (∫ (x : ℝ) in z₀.re..z.re, f { re := x, im := z₀.im }) = (∫ (x : ℝ) in z₀.re..z₁.re, f { re := x, im := z₀.im }) + (∫ (x : ℝ) in z₁.re..z.re, f { re := x, im := z₀.im }) := by
@@ -545,8 +500,26 @@ theorem primitive_additivity
   have H' : DifferentiableOn ℂ f (Set.uIcc z₁.re z.re ×ℂ Set.uIcc z₀.im z₁.im) := by
     apply DifferentiableOn.mono hf
     intro x hx
-    exact H hx
+    constructor
-
+    · simp
+      calc dist x.re z₀.re
+      _ ≤ dist x.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle x.re z₁.re z₀.re
+      _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by
+        apply (add_le_add_iff_right (dist z₁.re z₀.re)).mpr
+        rw [Set.uIcc_comm] at hx
+        apply Real.dist_right_le_of_mem_uIcc (Complex.mem_reProdIm.1 hx).1
+      _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
+        apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
+        apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
+      _ = rx := by
+        rw [dist_comm]
+        simp
+    · simp
+      calc dist x.im z₀.im
+      _ ≤ dist z₀.im z₁.im := by rw [dist_comm]; exact Real.dist_left_le_of_mem_uIcc (Complex.mem_reProdIm.1 hx).2
+      _ < ry := by
+        rw [dist_comm]
+        exact Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz₁).2
 
   let A := Complex.integral_boundary_rect_eq_zero_of_differentiableOn f ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ H'
   have {x : ℝ} {w : ℂ} : ↑x + w.im * Complex.I = { re := x, im := w.im } := by