From 103fd5fb0f62fafbdf491666799df7e89bcff8a5 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 2 Aug 2024 12:46:21 +0200
Subject: [PATCH] =?UTF-8?q?working=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Nevanlinna/holomorphic_primitive2.lean | 44 ++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean
index d3991ff..6a0d296 100644
--- a/Nevanlinna/holomorphic_primitive2.lean
+++ b/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]