Nevanlinna/holomorphic_primitive2.lean

@@ -289,30 +289,61 @@ theorem primitive_hasDerivAtBasepoint
   exact hasDerivAt_id z₀
 
 
+lemma integrability₁
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E)
+  (hf : Differentiable ℂ f)
+  (a₁ a₂ b : ℝ) :
+  IntervalIntegrable (fun x => f { re := x, im := b }) MeasureTheory.volume a₁ a₂ := by
+  apply Continuous.intervalIntegrable
+  apply Continuous.comp
+  exact Differentiable.continuous hf
+  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
+  rw [this]
+  continuity
+
+
+lemma integrability₂
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E)
+  (hf : Differentiable ℂ f)
+  (a₁ a₂ b : ℝ) :
+  IntervalIntegrable (fun x => f { re := b, im := x }) MeasureTheory.volume a₁ a₂ := by
+  apply Continuous.intervalIntegrable
+  apply Continuous.comp
+  exact Differentiable.continuous hf
+  have : (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
+  continuity
+  fun_prop
+
+
 theorem primitive_additivity
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  {z₀ : ℂ}
-  {rx ry : ℝ}
-  (hf : DifferentiableOn ℂ f (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry))
+  (f : ℂ  → E)
+  (z₀ : ℂ)
+  (rx ry : ℝ)
   (hry : 0 < ry)
-  {z₁ : ℂ}
+  (hf : DifferentiableOn ℂ f (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry))
+  (z₁ : ℂ)
   (hz₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry))
   :
-  ∃ εx > 0, ∃ εy > 0, ∀ z ∈ (Metric.ball z₁.re εx ×ℂ Metric.ball z₁.im εy), (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁) = 0 := by
-
-  let εx := rx - dist z₀.re z₁.re
-  have hεx : εx > 0 := by
-    sorry
-  let εy := ry - dist z₀.im z₁.im
-  have hεy : εy > 0 := by
-    sorry
-
-  use εx
-  use hεx
-  use εy
-  use hεy
+  ∃ εx εy : ℝ, ∀ z ∈ (Metric.ball z₁.re εx ×ℂ Metric.ball z₁.im εy), (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁) = 0 := by
 
+  use rx - dist z₀.re z₁.re
+  use ry - dist z₀.im z₁.im
   intro z hz
 
   unfold primitive
@@ -507,77 +538,27 @@ theorem primitive_additivity
 
 theorem primitive_additivity'
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  {z₀ z₁ : ℂ}
-  {R : ℝ}
+  (f : ℂ  → E)
+  (z₀ : ℂ)
+  (R : ℝ)
   (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
-  (hz₁ : z₁ ∈ Metric.ball z₀ R)
+  (z₁ : ℂ)
+  (hz₁ : z₁ ∈ (Metric.ball z₀ R))
   :
   primitive z₀ f =ᶠ[nhds z₁] fun z ↦ (primitive z₁ f z) + (primitive z₀ f z₁) := by
-
-  let ε := R - dist z₀ z₁
-
-  have hε : 0 < ε := by
-    dsimp [ε]
-    simp
-    exact Metric.mem_ball'.mp hz₁
-
-  let rx := dist z₀.re z₁.re + ε/(2 : ℝ)
-  let ry := dist z₀.im z₁.im + ε/(2 : ℝ)
-
-  have h'ry : 0 < ry := by
-    dsimp [ry]
-    apply add_pos_of_nonneg_of_pos
-    exact dist_nonneg
-    simpa
-
-  have h'f : DifferentiableOn ℂ f (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by
-    apply hf.mono
-    intro x hx
-    simp
-    let A := hx.1
-    simp at A
-    let B := hx.2
-    simp at B
-    calc dist x z₀
-    _ = √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) := by exact Complex.dist_eq_re_im x z₀
-    _ =
   sorry
 
-  have h'z₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by
-    dsimp [rx, ry]
-    constructor
-    · rw [dist_comm]; simp; exact hε
-    · rw [dist_comm]; simp; exact hε
-
-  obtain ⟨εx, hεx, εy, hεy, hε⟩ := primitive_additivity h'f h'ry h'z₁
-
-  apply Filter.eventuallyEq_iff_exists_mem.2
-  use (Metric.ball z₁.re εx ×ℂ Metric.ball z₁.im εy)
-  constructor
-  · apply IsOpen.mem_nhds
-    apply IsOpen.reProdIm
-    exact Metric.isOpen_ball
-    exact Metric.isOpen_ball
-    constructor
-    · simpa
-    · simpa
-  · intro x hx
-    simp
-    rw [← sub_zero (primitive z₀ f x), ← hε x hx]
-    abel
-
 
 theorem primitive_hasDerivAt
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  {z₀ z : ℂ}
-  {R : ℝ}
+  (f : ℂ  → E)
+  (z₀ z : ℂ)
+  (R : ℝ)
   (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
   (hz : z ∈ Metric.ball z₀ R) :
   HasDerivAt (primitive z₀ f) (f z) z := by
 
-  let A := primitive_additivity' hf hz
+  let A := primitive_additivity' f z₀ R hf z hz
   rw [Filter.EventuallyEq.hasDerivAt_iff A]
   rw [← add_zero (f z)]
   apply HasDerivAt.add
@@ -598,7 +579,7 @@ theorem primitive_differentiable
   DifferentiableOn ℂ (primitive z₀ f) (Metric.ball z₀ R) := by
   intro z hz
   apply DifferentiableAt.differentiableWithinAt
-  exact (primitive_hasDerivAt hf hz).differentiableAt
+  exact (primitive_hasDerivAt f z₀ z R hf hz).differentiableAt
 
 
 theorem primitive_hasFderivAt
@@ -612,27 +593,27 @@ theorem primitive_hasFderivAt
   intro z hz
   rw [hasFDerivAt_iff_hasDerivAt]
   simp
-  apply primitive_hasDerivAt hf hz
+  apply primitive_hasDerivAt f z₀ z R hf hz
 
 
 theorem primitive_hasFderivAt'
   {f : ℂ  → ℂ}
-  {z₀ : ℂ}
-  {R : ℝ}
+  (z₀ : ℂ)
+  (R : ℝ)
   (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
   :
   ∀ z ∈ Metric.ball z₀ R, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul ℂ ℂ (f z)) z := by
   intro z hz
   rw [hasFDerivAt_iff_hasDerivAt]
   simp
-  exact primitive_hasDerivAt hf hz
+  exact primitive_hasDerivAt f z₀ z R hf hz
 
 
 theorem primitive_fderiv
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   {f : ℂ  → E}
-  {z₀ : ℂ}
-  {R : ℝ}
+  (z₀ : ℂ)
+  (R : ℝ)
   (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
   :
   ∀ z ∈ Metric.ball z₀ R, (fderiv ℂ (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ℂ ℂ).flip (f z) := by
@@ -643,11 +624,11 @@ theorem primitive_fderiv
 
 theorem primitive_fderiv'
   {f : ℂ  → ℂ}
-  {z₀ : ℂ}
-  {R : ℝ}
+  (z₀ : ℂ)
+  (R : ℝ)
   (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
   :
   ∀ z ∈ Metric.ball z₀ R, (fderiv ℂ (primitive z₀ f) z) = ContinuousLinearMap.lsmul ℂ ℂ (f z) := by
   intro z hz
   apply HasFDerivAt.fderiv
-  exact primitive_hasFderivAt' hf z hz
+  exact primitive_hasFderivAt' z₀ R hf z hz