Working…

Nevanlinna/holomorphic_primitive2.lean

@@ -0,0 +1,456 @@
+import Mathlib.Analysis.Complex.TaylorSeries
+
+
+noncomputable def primitive
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] :
+  ℂ  → (ℂ → E) → (ℂ → E) := by
+  intro z₀
+  intro f
+  exact fun z ↦ (∫ (x : ℝ) in z₀.re..z.re, f ⟨x, z₀.im⟩) + Complex.I • ∫ (x : ℝ) in z₀.im..z.im, f ⟨z.re, x⟩
+
+
+theorem primitive_zeroAtBasepoint
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E)
+  (z₀ : ℂ) :
+  (primitive z₀ f) z₀ = 0 := by
+  unfold primitive
+  simp
+
+
+theorem primitive_fderivAtBasepointZero
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E)
+  (hf : Continuous f) :
+  HasDerivAt (primitive 0 f) (f 0) 0 := by
+  unfold primitive
+  simp
+  apply hasDerivAt_iff_isLittleO.2
+  simp
+  rw [Asymptotics.isLittleO_iff]
+  intro c hc
+
+  have {z : ℂ} {e : E} : z • e = (∫ (_ : ℝ) in (0)..(z.re), e) + Complex.I • ∫ (_ : ℝ) in (0)..(z.im), e:= by
+    simp
+    rw [smul_comm]
+    rw [← smul_assoc]
+    simp
+    have : z.re • e = (z.re : ℂ) • e := by exact rfl
+    rw [this, ← add_smul]
+    simp
+  conv =>
+    left
+    intro x
+    left
+    arg 1
+    arg 2
+    rw [this]
+  have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
+    abel
+  have t₀ {r : ℝ} : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := by
+    apply Continuous.intervalIntegrable
+    apply Continuous.comp
+    exact hf
+    have : (fun x => ({ re := x, im := 0 } : ℂ)) = Complex.ofRealLI := by rfl
+    rw [this]
+    continuity
+  have t₁ {r : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by
+    apply Continuous.intervalIntegrable
+    apply Continuous.comp
+    exact hf
+    fun_prop
+  have t₂ {a b : ℝ} : IntervalIntegrable (fun x_1 => f { re := a, im := x_1 }) MeasureTheory.volume 0 b := by
+    apply Continuous.intervalIntegrable
+    apply Continuous.comp hf
+    have : (Complex.mk a) = (fun x => Complex.I • Complex.ofRealCLM x + { re := a, im := 0 }) := by
+      funext x
+      apply Complex.ext
+      rw [Complex.add_re]
+      simp
+      simp
+    rw [this]
+    apply Continuous.add
+    continuity
+    fun_prop
+
+  have t₃ {a : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 a := by
+    apply Continuous.intervalIntegrable
+    apply Continuous.comp
+    exact hf
+    fun_prop
+  conv =>
+    left
+    intro x
+    left
+    arg 1
+    rw [this]
+    rw [← smul_sub]
+    rw [← intervalIntegral.integral_sub t₀ t₁]
+    rw [← intervalIntegral.integral_sub t₂ t₃]
+  rw [Filter.eventually_iff_exists_mem]
+
+  let s := f⁻¹' Metric.ball (f 0) (c / (4 : ℝ))
+  have h₁s : IsOpen s := IsOpen.preimage hf Metric.isOpen_ball
+  have h₂s : 0 ∈ s := by
+    apply Set.mem_preimage.mpr
+    apply Metric.mem_ball_self
+    linarith
+
+  obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 h₁s 0 h₂s
+
+  have h₃ε : ∀ y ∈ Metric.ball 0 ε, ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by
+    intro y hy
+    apply mem_ball_iff_norm.mp (h₂ε hy)
+
+  use Metric.ball 0 (ε / (4 : ℝ))
+  constructor
+  · apply Metric.ball_mem_nhds 0
+    linarith
+  · intro y hy
+    have h₁y : |y.re| < ε / 4 := by
+      calc |y.re|
+      _ ≤ Complex.abs y := by apply Complex.abs_re_le_abs
+      _ < ε / 4 := by
+        let A := mem_ball_iff_norm.1 hy
+        simp at A
+        linarith
+    have h₂y : |y.im| < ε / 4 := by
+      calc |y.im|
+      _ ≤ Complex.abs y := by apply Complex.abs_im_le_abs
+      _ < ε / 4 := by
+        let A := mem_ball_iff_norm.1 hy
+        simp at A
+        linarith
+
+    have intervalComputation {x' y' : ℝ} (h : x' ∈ Ι 0 y') : |x'| ≤ |y'| := by
+      let A := h.1
+      let B := h.2
+      rcases le_total 0 y' with hy | hy
+      · simp [hy] at A
+        simp [hy] at B
+        rw [abs_of_nonneg hy]
+        rw [abs_of_nonneg (le_of_lt A)]
+        exact B
+      · simp [hy] at A
+        simp [hy] at B
+        rw [abs_of_nonpos hy]
+        rw [abs_of_nonpos]
+        linarith [h.1]
+        exact B
+
+    have t₁ : ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ (c / (4 : ℝ)) * |y.re - 0| := by
+      apply intervalIntegral.norm_integral_le_of_norm_le_const
+      intro x hx
+
+      have h₁x : |x| < ε / 4 := by
+        calc |x|
+          _ ≤ |y.re| := intervalComputation hx
+          _ < ε / 4 := h₁y
+      apply le_of_lt
+      apply h₃ε { re := x, im := 0 }
+      rw [mem_ball_iff_norm]
+      simp
+      have : { re := x, im := 0 } = (x : ℂ) := by rfl
+      rw [this]
+      rw [Complex.abs_ofReal]
+      linarith
+
+    have t₂ : ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ ≤ (c / (4 : ℝ)) * |y.im - 0| := by
+      apply intervalIntegral.norm_integral_le_of_norm_le_const
+      intro x hx
+
+      have h₁x : |x| < ε / 4 := by
+        calc |x|
+          _ ≤ |y.im| := intervalComputation hx
+          _ < ε / 4 := h₂y
+
+      apply le_of_lt
+      apply h₃ε { re := y.re, im := x }
+      simp
+
+      calc Complex.abs { re := y.re, im := x }
+        _ ≤ |y.re| + |x| := by
+          apply Complex.abs_le_abs_re_add_abs_im { re := y.re, im := x }
+        _ < ε := by
+          linarith
+
+    calc ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0) + Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖
+      _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
+        apply norm_add_le
+      _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
+        simp
+        rw [norm_smul]
+        simp
+      _ ≤ (c / (4 : ℝ)) * |y.re - 0| + (c / (4 : ℝ)) * |y.im - 0| := by
+        apply add_le_add
+        exact t₁
+        exact t₂
+      _ ≤ (c / (4 : ℝ)) * (|y.re| + |y.im|) := by
+        simp
+        rw [mul_add]
+      _ ≤ (c / (4 : ℝ)) * (4 * ‖y‖) := by
+        have : |y.re| + |y.im| ≤ 4 * ‖y‖ := by
+          calc |y.re| + |y.im|
+            _ ≤ ‖y‖ + ‖y‖ := by
+              apply add_le_add
+              apply Complex.abs_re_le_abs
+              apply Complex.abs_im_le_abs
+            _ ≤ 4 * ‖y‖ := by
+              rw [← two_mul]
+              apply mul_le_mul
+              linarith
+              rfl
+              exact norm_nonneg y
+              linarith
+
+        apply mul_le_mul
+        rfl
+        exact this
+        apply add_nonneg
+        apply abs_nonneg
+        apply abs_nonneg
+        linarith
+      _ ≤ c * ‖y‖ := by
+        linarith
+
+
+theorem primitive_translation
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E)
+  (z₀ t : ℂ) :
+  primitive z₀ (f ∘ fun z ↦ (z - t)) = ((primitive (z₀ - t) f) ∘ fun z ↦ (z - t)) := by
+  funext z
+  unfold primitive
+  simp
+
+  let g : ℝ → E := fun x ↦ f ( {re := x, im := z₀.im - t.im} )
+  have {x : ℝ} : f ({ re := x, im := z₀.im } - t) = g (1*x - t.re) := by
+    congr 1
+    apply Complex.ext <;> simp
+  conv =>
+    left
+    left
+    arg 1
+    intro x
+    rw [this]
+  rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.re)]
+  simp
+
+  congr 1
+  let g : ℝ → E := fun x ↦ f ( {re := z.re - t.re, im := x} )
+  have {x : ℝ} : f ({ re := z.re, im := x} - t) = g (1*x - t.im) := by
+    congr 1
+    apply Complex.ext <;> simp
+  conv =>
+    left
+    arg 1
+    intro x
+    rw [this]
+  rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.im)]
+  simp
+
+
+theorem primitive_hasDerivAtBasepoint
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  {f : ℂ  → E}
+  (hf : Continuous f)
+  (z₀ : ℂ) :
+  HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
+
+  let g := f ∘ fun z ↦ z + z₀
+  have : Continuous g := by continuity
+  let A := primitive_fderivAtBasepointZero g this
+  simp at A
+
+  let B := primitive_translation g z₀ z₀
+  simp at B
+  have : (g ∘ fun z ↦ (z - z₀)) = f := by
+    funext z
+    dsimp [g]
+    simp
+  rw [this] at B
+  rw [B]
+  have : f z₀ = (1 : ℂ) • (f z₀) := by
+    exact (MulAction.one_smul (f z₀)).symm
+  conv =>
+    arg 2
+    rw [this]
+
+  apply HasDerivAt.scomp
+  simp
+  have : g 0 = f z₀ := by simp [g]
+  rw [← this]
+  exact A
+  apply HasDerivAt.sub_const
+  have : (fun (x : ℂ) ↦ x) = id := by
+    funext x
+    simp
+  rw [this]
+  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)
+  (hf : Differentiable ℂ f)
+  (z₀ z₁ : ℂ) :
+  (fun z ↦ (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁)) = 0 := by
+  funext z
+
+
+
+  unfold primitive
+  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]
+    apply integrability₁ f hf
+    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]
+    apply integrability₂ f hf
+    apply integrability₂ f hf
+  rw [this]
+  simp
+
+  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
+
+  let A := Complex.integral_boundary_rect_eq_zero_of_differentiableOn f ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ (hf.differentiableOn)
+  have {x : ℝ} {w : ℂ} : ↑x + w.im * Complex.I = { re := x, im := w.im } := by
+    apply Complex.ext
+    · simp
+    · simp
+  simp_rw [this] at A
+  have {x : ℝ} {w : ℂ} : w.re + x * Complex.I = { re := w.re, im := x } := by
+    apply Complex.ext
+    · simp
+    · simp
+  simp_rw [this] at A
+  rw [← A]
+  abel
+
+
+theorem primitive_additivity'
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E)
+  (hf : Differentiable ℂ f)
+  (z₀ z₁ : ℂ) :
+  primitive z₀ f = fun z ↦ (primitive z₁ f) z + (primitive z₀ f z₁) := by
+
+  nth_rw 1 [← sub_zero (primitive z₀ f)]
+  rw [← primitive_additivity f hf z₀ z₁]
+
+  funext z
+  simp
+  abel
+
+
+theorem primitive_hasDerivAt
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  {f : ℂ  → E}
+  (hf : Differentiable ℂ f)
+  (z₀ z : ℂ) :
+  HasDerivAt (primitive z₀ f) (f z) z := by
+  rw [primitive_additivity' f hf z₀ z]
+  rw [← add_zero (f z)]
+  apply HasDerivAt.add
+  apply primitive_hasDerivAtBasepoint
+  exact hf.continuous
+  apply hasDerivAt_const
+
+
+theorem primitive_differentiable
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  {f : ℂ  → E}
+  (hf : Differentiable ℂ f)
+  (z₀ : ℂ) :
+  Differentiable ℂ (primitive z₀ f) := by
+  intro z
+  exact (primitive_hasDerivAt hf z₀ z).differentiableAt
+
+
+theorem primitive_hasFderivAt
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  {f : ℂ  → E}
+  (hf : Differentiable ℂ f)
+  (z₀ : ℂ) :
+  ∀ z, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ℂ ℂ).flip (f z)) z := by
+  intro z
+  rw [hasFDerivAt_iff_hasDerivAt]
+  simp
+  exact primitive_hasDerivAt hf z₀ z
+
+
+theorem primitive_hasFderivAt'
+  {f : ℂ  → ℂ}
+  (hf : Differentiable ℂ f)
+  (z₀ : ℂ) :
+  ∀ z, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul ℂ ℂ (f z)) z := by
+  intro z
+  rw [hasFDerivAt_iff_hasDerivAt]
+  simp
+  exact primitive_hasDerivAt hf z₀ z
+
+
+theorem primitive_fderiv
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  {f : ℂ  → E}
+  (hf : Differentiable ℂ f)
+  (z₀ : ℂ) :
+  ∀ z, (fderiv ℂ (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ℂ ℂ).flip (f z) := by
+  intro z
+  apply HasFDerivAt.fderiv
+  exact primitive_hasFderivAt hf z₀ z
+
+
+theorem primitive_fderiv'
+  {f : ℂ  → ℂ}
+  (hf : Differentiable ℂ f)
+  (z₀ : ℂ) :
+  ∀ z, (fderiv ℂ (primitive z₀ f) z) = ContinuousLinearMap.lsmul ℂ ℂ (f z) := by
+  intro z
+  apply HasFDerivAt.fderiv
+  exact primitive_hasFderivAt' hf z₀ z