Nevanlinna/holomorphic_primitive2.lean

@@ -337,107 +337,13 @@ theorem primitive_additivity
   (R : ℝ)
   (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
   (z₁ : ℂ)
-  (hz₁ : z₁ ∈ Metric.ball z₀ R)
+  (hz₁ : z₁ ∈ Metric.ball z₀ R) :
-  :
+  ∀ z ∈ Metric.ball z₁ (R - ‖z₁‖), (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁) = 0 := by
-  ∀ z ∈ Metric.ball z₁ (R - dist z₁ z₀), (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁) = 0 := by
+  intro z _
-  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₀ : x.re ∈ Set.uIcc z₁.re z.re := by exact (Complex.mem_reProdIm.1 hx).1
-    have a₁ : x.im ∈ Set.uIcc z₀.im z₁.im := by exact (Complex.mem_reProdIm.1 hx).2
-
-
-    have A₀ : dist x.re z₀.re ≤ dist x.re z₁.re + dist z₁.re z₀.re := by apply dist_triangle
-
-    have A₁ : dist x.im z₀.im ≤ dist z₁.im z₀.im := by
-      apply Real.dist_right_le_of_mem_uIcc
-      rwa [Set.uIcc_comm]
-
-    have A₂ : dist x.re z₁.re ≤ dist z.re z₁.re := by
-      apply Real.dist_right_le_of_mem_uIcc
-      rwa [Set.uIcc_comm]
-
-    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 x z₀ ≤ dist x ⟨z₁.re, x.im⟩ + dist ⟨z₁.re, x.im⟩ z₀ := by apply dist_triangle
-
-    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 integrability₁
-    (a₁ a₂ b : ℝ) :
-    IntervalIntegrable (fun x => f { re := x, im := b }) MeasureTheory.volume a₁ a₂ := by
-    apply ContinuousOn.intervalIntegrable
-    apply ContinuousOn.comp
-    exact hf.continuousOn
-
-    have : ((fun x => { re := x, im := b }) : ℝ → ℂ) = (fun x => Complex.ofRealCLM x + { re := 0, im := b }) := by
-      funext x
-      apply Complex.ext
-      rw [Complex.add_re]
-      simp
-      rw [Complex.add_im]
-      simp
-    apply Continuous.continuousOn
-    rw [this]
-    continuity
-    --
-    intro w hw
-    simp
-    rw [Complex.dist_eq_re_im]
-
   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
     rw [intervalIntegral.integral_add_adjacent_intervals]
-    -- IntervalIntegrable (fun x => f { re := x, im := z₀.im }) MeasureTheory.volume z₀.re z₁.re
-    apply ContinuousOn.intervalIntegrable
-    apply ContinuousOn.comp
-    exact hf.continuousOn
-    have {b : ℝ} : ((fun x => { re := x, im := b }) : ℝ → ℂ) = (fun x => Complex.ofRealCLM x + { re := 0, im := b }) := by
-      funext x
-      apply Complex.ext
-      rw [Complex.add_re]
-      simp
-      rw [Complex.add_im]
-      simp
-    apply Continuous.continuousOn
-    rw [this]
-    continuity
-    -- Remains: Set.MapsTo (fun x => { re := x, im := z₀.im }) (Set.uIcc z₀.re z₁.re) (Metric.ball z₀ R)
-    intro w hw
-    simp
-
-
-
     sorry --apply integrability₁ f hf
     sorry --apply integrability₁ f hf
   rw [this]
@@ -457,10 +363,9 @@ theorem primitive_additivity
     apply DifferentiableOn.mono hf
     intro x hx
     simp
-
+    
     let A₀ : dist x.re z₀.re ≤ dist x.re z₁.re + dist z₁.re z₀.re := by apply dist_triangle
-    let A₁ : dist x.im z₀.im ≤ dist z₁.im z₀.im := by sorry
+    
-