working…

Nevanlinna/holomorphic_primitive2.lean

@@ -392,8 +392,52 @@ 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
+    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]