Update holomorphic_primitive2.lean

Nevanlinna/holomorphic_primitive2.lean

@@ -393,31 +393,10 @@ theorem primitive_additivity
 
   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
@@ -432,18 +411,71 @@ theorem primitive_additivity
     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)
+    -- -- Remains: Set.MapsTo (fun x => { re := x, im := z₀.im }) (Set.uIcc z₀.re z₁.re) (Metric.ball z₀ R)
+    intro w hw
+    simp
+    simp_rw [Complex.dist_of_im_eq]
+    calc dist w z₀.re
+      _ ≤ dist z₁.re z₀.re := by apply Real.dist_right_le_of_mem_uIcc; rwa [Set.uIcc_comm] at hw
+      _ ≤ dist z₁ z₀ := by sorry
+      _ < R := by simp at hz₁; assumption
+
+    -- 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
+    simp_rw [Complex.dist_of_im_eq]
+    calc dist w z₀.re
+      _ ≤ dist w z₁.re + dist z₁.re z₀.re := by exact dist_triangle w z₁.re z₀.re
+      _ ≤ dist z₁.re z.re + dist z₁.re z₀.re := by
+        apply add_le_add_right
+        apply Real.dist_le_of_mem_uIcc hw
+        simp
+      _ ≤ dist z₁ z + dist z₁ z₀ := by
+        sorry
+      _ < (R - dist z₁ z₀) + dist z₁ z₀ := by
+        apply add_lt_add_right
+        simp at hz
+        rwa [dist_comm]
+      _ = R := by simp
+  rw [this]
+
+  have : (∫ (x : ℝ) in z₀.im..z.im, f { re := z.re, im := x }) = (∫ (x : ℝ) in z₀.im..z₁.im, f { re := z.re, im := x }) + (∫ (x : ℝ) in z₁.im..z.im, f { re := z.re, im := x }) := by
+    rw [intervalIntegral.integral_add_adjacent_intervals]
+    -- IntervalIntegrable (fun x => f { re := z.re, im := x }) MeasureTheory.volume z₀.im z₁.im
+    apply ContinuousOn.intervalIntegrable
+    apply ContinuousOn.comp
+    exact hf.continuousOn
+    apply Continuous.continuousOn
+    have {b : ℝ}:  (Complex.mk b) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by
+      funext x
+      apply Complex.ext
+      rw [Complex.add_re]
+      simp
+      simp
+    rw [this]
+    apply Continuous.add
+    fun_prop
+    fun_prop
+    -- Set.MapsTo (Complex.mk z.re) (Set.uIcc z₀.im z₁.im) (Metric.ball z₀ R)
     intro w hw
     simp
 
-
-
-    sorry --apply integrability₁ f hf
-    sorry --apply integrability₁ f hf
-  rw [this]
-  have : (∫ (x : ℝ) in z₀.im..z.im, f { re := z.re, im := x }) = (∫ (x : ℝ) in z₀.im..z₁.im, f { re := z.re, im := x }) + (∫ (x : ℝ) in z₁.im..z.im, f { re := z.re, im := x }) := by
-    rw [intervalIntegral.integral_add_adjacent_intervals]
     sorry --apply integrability₂ f hf
+
     sorry --apply integrability₂ f hf
   rw [this]
   simp
@@ -451,22 +483,16 @@ theorem primitive_additivity
   have {a b c d e f g h : E} : (a + b) + (c + d) - (e + f) - (g + h) = b + (a - g) - e - f + d  - h + (c) := by
     abel
   rw [this]
-  simp
 
-  have H : DifferentiableOn ℂ f (Set.uIcc z₁.re z.re ×ℂ Set.uIcc z₀.im z₁.im) := by
+
+  have H' : DifferentiableOn ℂ f (Set.uIcc z₁.re z.re ×ℂ Set.uIcc z₀.im z₁.im) := by
     apply DifferentiableOn.mono hf
     intro x hx
     simp
-
+    exact H hx
-    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
 
 
-
+  let A := Complex.integral_boundary_rect_eq_zero_of_differentiableOn f ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ H'
-
-    sorry
-
-  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
     apply Complex.ext
     · simp