From 75ce3b31ef9df189e924e22321a0dcb9e7b07026 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 8 Aug 2024 13:32:15 +0200 Subject: [PATCH] working --- Nevanlinna/holomorphic_primitive.lean | 976 ++++++++++++--------- Nevanlinna/holomorphic_primitive2.lean | 846 ------------------ Nevanlinna/junk/holomorphic_primitive.lean | 666 ++++++++++++++ 3 files changed, 1244 insertions(+), 1244 deletions(-) delete mode 100644 Nevanlinna/holomorphic_primitive2.lean create mode 100644 Nevanlinna/junk/holomorphic_primitive.lean diff --git a/Nevanlinna/holomorphic_primitive.lean b/Nevanlinna/holomorphic_primitive.lean index 9b393cc..640ee43 100644 --- a/Nevanlinna/holomorphic_primitive.lean +++ b/Nevanlinna/holomorphic_primitive.lean @@ -1,240 +1,5 @@ import Mathlib.Analysis.Complex.TaylorSeries -import Mathlib.Analysis.SpecialFunctions.Integrals -import Mathlib.MeasureTheory.Integral.DivergenceTheorem -import Mathlib.MeasureTheory.Integral.IntervalIntegral -import Mathlib.MeasureTheory.Function.LocallyIntegrable -import Nevanlinna.partialDeriv -import Nevanlinna.cauchyRiemann - -/- -noncomputable def partialDeriv - {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] - {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] : E → (E → F) → (E → F) := - fun v ↦ (fun f ↦ (fun w ↦ fderiv ℝ f w v)) - - -theorem partialDeriv_compContLinAt - {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] - {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] - {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] - {f : E → F} - {l : F →L[ℝ] G} - {v : E} - {x : E} - (h : DifferentiableAt ℝ f x) : - (partialDeriv v (l ∘ f)) x = (l ∘ partialDeriv v f) x:= by - unfold partialDeriv - rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h] - simp - - -theorem partialDeriv_compCLE - {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] - {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] - {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] - {f : E → F} - {l : F ≃L[ℝ] G} {v : E} : partialDeriv v (l ∘ f) = l ∘ partialDeriv v f := by - funext x - by_cases hyp : DifferentiableAt ℝ f x - · let lCLM : F →L[ℝ] G := l - suffices shyp : partialDeriv v (lCLM ∘ f) x = (lCLM ∘ partialDeriv v f) x from by tauto - apply partialDeriv_compContLinAt - exact hyp - · unfold partialDeriv - rw [fderiv_zero_of_not_differentiableAt] - simp - rw [fderiv_zero_of_not_differentiableAt] - simp - exact hyp - rw [ContinuousLinearEquiv.comp_differentiableAt_iff] - exact hyp - -theorem partialDeriv_smul'₂ - {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] - {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] - {f : E → F} {a : ℂ} {v : E} : - partialDeriv v (a • f) = a • partialDeriv v f := by - - funext w - by_cases ha : a = 0 - · unfold partialDeriv - have : a • f = fun y ↦ a • f y := by rfl - rw [this, ha] - simp - · -- Now a is not zero. We present scalar multiplication with a as a continuous linear equivalence. - let smulCLM : F ≃L[ℝ] F := - { - toFun := fun x ↦ a • x - map_add' := fun x y => DistribSMul.smul_add a x y - map_smul' := fun m x => (smul_comm ((RingHom.id ℝ) m) a x).symm - invFun := fun x ↦ a⁻¹ • x - left_inv := by - intro x - simp - rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel ha, one_smul] - right_inv := by - intro x - simp - rw [← smul_assoc, smul_eq_mul, mul_inv_cancel ha, one_smul] - continuous_toFun := continuous_const_smul a - continuous_invFun := continuous_const_smul a⁻¹ - } - - have : a • f = smulCLM ∘ f := by tauto - rw [this] - rw [partialDeriv_compCLE] - tauto - -theorem CauchyRiemann₄ - {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] - {f : ℂ → F} : - (Differentiable ℂ f) → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by - intro h - unfold partialDeriv - - conv => - left - intro w - rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)] - simp - rw [← mul_one Complex.I] - rw [← smul_eq_mul] - conv => - right - right - intro w - rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)] - funext w - simp --/ - - -theorem MeasureTheory.integral2_divergence₃ - {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] - (f g : ℝ × ℝ → E) - (h₁f : ContDiff ℝ 1 f) - (h₁g : ContDiff ℝ 1 g) - (a₁ : ℝ) - (a₂ : ℝ) - (b₁ : ℝ) - (b₂ : ℝ) : - ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, ((fderiv ℝ f) (x, y)) (1, 0) + ((fderiv ℝ g) (x, y)) (0, 1) = (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) - ∫ (y : ℝ) in a₂..b₂, f (a₁, y) := by - - apply integral2_divergence_prod_of_hasFDerivWithinAt_off_countable f g (fderiv ℝ f) (fderiv ℝ g) a₁ a₂ b₁ b₂ ∅ - exact Set.countable_empty - -- ContinuousOn f (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂) - exact h₁f.continuous.continuousOn - -- - exact h₁g.continuous.continuousOn - -- - rw [Set.diff_empty] - intro x _ - exact DifferentiableAt.hasFDerivAt ((h₁f.differentiable le_rfl) x) - -- - rw [Set.diff_empty] - intro y _ - exact DifferentiableAt.hasFDerivAt ((h₁g.differentiable le_rfl) y) - -- - apply ContinuousOn.integrableOn_compact - apply IsCompact.prod - exact isCompact_uIcc - exact isCompact_uIcc - apply ContinuousOn.add - apply Continuous.continuousOn - exact Continuous.clm_apply (ContDiff.continuous_fderiv h₁f le_rfl) continuous_const - apply Continuous.continuousOn - exact Continuous.clm_apply (ContDiff.continuous_fderiv h₁g le_rfl) continuous_const - - -theorem integral_divergence₄ - {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] - (f g : ℂ → E) - (h₁f : ContDiff ℝ 1 f) - (h₁g : ContDiff ℝ 1 g) - (a₁ : ℝ) - (a₂ : ℝ) - (b₁ : ℝ) - (b₂ : ℝ) : - ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, ((fderiv ℝ f) ⟨x, y⟩ ) 1 + ((fderiv ℝ g) ⟨x, y⟩) Complex.I = (((∫ (x : ℝ) in a₁..b₁, g ⟨x, b₂⟩) - ∫ (x : ℝ) in a₁..b₁, g ⟨x, a₂⟩) + ∫ (y : ℝ) in a₂..b₂, f ⟨b₁, y⟩) - ∫ (y : ℝ) in a₂..b₂, f ⟨a₁, y⟩ := by - - let fr : ℝ × ℝ → E := f ∘ Complex.equivRealProdCLM.symm - let gr : ℝ × ℝ → E := g ∘ Complex.equivRealProdCLM.symm - - have sfr {x y : ℝ} : f { re := x, im := y } = fr (x, y) := by exact rfl - have sgr {x y : ℝ} : g { re := x, im := y } = gr (x, y) := by exact rfl - repeat (conv in f { re := _, im := _ } => rw [sfr]) - repeat (conv in g { re := _, im := _ } => rw [sgr]) - - have sfr' {x y : ℝ} {z : ℂ} : (fderiv ℝ f { re := x, im := y }) z = fderiv ℝ fr (x, y) (Complex.equivRealProdCLM z) := by - rw [fderiv.comp] - rw [Complex.equivRealProdCLM.symm.fderiv] - tauto - apply Differentiable.differentiableAt - exact h₁f.differentiable le_rfl - exact Complex.equivRealProdCLM.symm.differentiableAt - conv in ⇑(fderiv ℝ f { re := _, im := _ }) _ => rw [sfr'] - - have sgr' {x y : ℝ} {z : ℂ} : (fderiv ℝ g { re := x, im := y }) z = fderiv ℝ gr (x, y) (Complex.equivRealProdCLM z) := by - rw [fderiv.comp] - rw [Complex.equivRealProdCLM.symm.fderiv] - tauto - apply Differentiable.differentiableAt - exact h₁g.differentiable le_rfl - exact Complex.equivRealProdCLM.symm.differentiableAt - conv in ⇑(fderiv ℝ g { re := _, im := _ }) _ => rw [sgr'] - - apply MeasureTheory.integral2_divergence₃ fr gr _ _ a₁ a₂ b₁ b₂ - -- ContDiff ℝ 1 fr - exact (ContinuousLinearEquiv.contDiff_comp_iff (ContinuousLinearEquiv.symm Complex.equivRealProdCLM)).mpr h₁f - -- ContDiff ℝ 1 gr - exact (ContinuousLinearEquiv.contDiff_comp_iff (ContinuousLinearEquiv.symm Complex.equivRealProdCLM)).mpr h₁g - - -theorem integral_divergence₅ - {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] - (F : ℂ → E) - (hF : Differentiable ℂ F) - (lowerLeft upperRight : ℂ) : - (∫ (x : ℝ) in lowerLeft.re..upperRight.re, F ⟨x, lowerLeft.im⟩) + Complex.I • ∫ (x : ℝ) in lowerLeft.im..upperRight.im, F ⟨upperRight.re, x⟩ = - (∫ (x : ℝ) in lowerLeft.re..upperRight.re, F ⟨x, upperRight.im⟩) + Complex.I • ∫ (x : ℝ) in lowerLeft.im..upperRight.im, F ⟨lowerLeft.re, x⟩ := by - - let h₁f : ContDiff ℝ 1 F := (hF.contDiff : ContDiff ℂ 1 F).restrict_scalars ℝ - - let h₁g : ContDiff ℝ 1 (-Complex.I • F) := by - have : -Complex.I • F = fun x ↦ -Complex.I • F x := by rfl - rw [this] - apply ContDiff.comp - exact contDiff_const_smul _ - exact h₁f - - let A := integral_divergence₄ (-Complex.I • F) F h₁g h₁f lowerLeft.re upperRight.im upperRight.re lowerLeft.im - have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv ℝ Complex.I F z := by rfl - conv at A in (fderiv ℝ F _) _ => rw [this] - have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv ℝ 1 (-Complex.I • F) z := by rfl - conv at A in (fderiv ℝ (-Complex.I • F) _) _ => rw [this] - conv at A => - left - arg 1 - intro x - arg 1 - intro y - rw [CauchyRiemann₄ hF] - rw [partialDeriv_smul'₂] - simp - simp at A - - have {t₁ t₂ t₃ t₄ : E} : 0 = (t₁ - t₂) + t₃ + t₄ → t₁ + t₃ = t₂ - t₄ := by - intro hyp - calc - t₁ + t₃ = t₁ + t₃ - 0 := by rw [sub_zero (t₁ + t₃)] - _ = t₁ + t₃ - (t₁ - t₂ + t₃ + t₄) := by rw [hyp] - _ = t₂ - t₄ := by abel - let B := this A - repeat - rw [intervalIntegral.integral_symm lowerLeft.im upperRight.im] at B - simp at B - exact B - +import Mathlib.Data.ENNReal.Basic noncomputable def primitive {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] : @@ -255,8 +20,10 @@ theorem primitive_zeroAtBasepoint theorem primitive_fderivAtBasepointZero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] - (f : ℂ → E) - (hf : Continuous f) : + {f : ℂ → E} + {R : ℝ} + (hR : 0 < R) + (hf : ContinuousOn f (Metric.ball 0 R)) : HasDerivAt (primitive 0 f) (f 0) 0 := by unfold primitive simp @@ -280,68 +47,180 @@ theorem primitive_fderivAtBasepointZero 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 + + obtain ⟨s, h₁s, h₂s⟩ : ∃ s ⊆ f⁻¹' Metric.ball (f 0) (c / (4 : ℝ)), IsOpen s ∧ 0 ∈ s := by + apply eventually_nhds_iff.mp + apply continuousAt_def.1 + apply Continuous.continuousAt 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] + apply continuousAt_def.1 + apply hf.continuousAt + exact Metric.ball_mem_nhds 0 hR + apply Metric.ball_mem_nhds (f 0) + simpa - 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₂ε⟩ : ∃ ε > 0, (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ s ∧ (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ Metric.ball 0 R := by + obtain ⟨ε', h₁ε', h₂ε'⟩ : ∃ ε' > 0, Metric.ball 0 ε' ⊆ s ∩ Metric.ball 0 R := by + apply Metric.mem_nhds_iff.mp + apply IsOpen.mem_nhds + apply IsOpen.inter + exact h₂s.1 + exact Metric.isOpen_ball + constructor + · exact h₂s.2 + · simpa - obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 h₁s 0 h₂s + use (2 : ℝ)⁻¹ * ε' - have h₃ε : ∀ y ∈ Metric.ball 0 ε, ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by + constructor + · simpa + · constructor + · intro x hx + apply (h₂ε' _).1 + simp + calc Complex.abs x + _ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x + _ < (2 : ℝ)⁻¹ * ε' + |x.im| := by + apply (add_lt_add_iff_right |x.im|).mpr + have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1 + simp at this + exact this + _ < (2 : ℝ)⁻¹ * ε' + (2 : ℝ)⁻¹ * ε' := by + apply (add_lt_add_iff_left ((2 : ℝ)⁻¹ * ε')).mpr + have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2 + simp at this + exact this + _ = ε' := by + rw [← add_mul] + abel_nf + simp + · intro x hx + apply (h₂ε' _).2 + simp + calc Complex.abs x + _ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x + _ < (2 : ℝ)⁻¹ * ε' + |x.im| := by + apply (add_lt_add_iff_right |x.im|).mpr + have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1 + simp at this + exact this + _ < (2 : ℝ)⁻¹ * ε' + (2 : ℝ)⁻¹ * ε' := by + apply (add_lt_add_iff_left ((2 : ℝ)⁻¹ * ε')).mpr + have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2 + simp at this + exact this + _ = ε' := by + rw [← add_mul] + abel_nf + simp + + have h₃ε : ∀ y ∈ (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε), ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by intro y hy - apply mem_ball_iff_norm.mp (h₂ε hy) + apply mem_ball_iff_norm.mp + apply h₁s + exact h₂ε.1 hy + + have intervalComputation_uIcc {x' y' : ℝ} (h : x' ∈ Set.uIcc 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 + rwa [abs_of_nonneg A, abs_of_nonneg hy] + · simp [hy] at A + simp [hy] at B + rw [abs_of_nonpos hy] + rw [abs_of_nonpos] + linarith [h.1] + exact B + + + rw [Filter.eventually_iff_exists_mem] use Metric.ball 0 (ε / (4 : ℝ)) + constructor · apply Metric.ball_mem_nhds 0 linarith · intro y hy + + have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by + abel + rw [this] + rw [← smul_sub] + + + have t₀ : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 y.re := by + apply ContinuousOn.intervalIntegrable + apply ContinuousOn.comp + exact hf + have : (fun x => ({ re := x, im := 0 } : ℂ)) = Complex.ofRealLI := by rfl + rw [this] + apply Continuous.continuousOn + continuity + intro x hx + apply h₂ε.2 + simp + constructor + · simp + calc |x| + _ ≤ |y.re| := by apply intervalComputation_uIcc hx + _ ≤ Complex.abs y := by exact Complex.abs_re_le_abs y + _ < ε / 4 := by simp at hy; assumption + _ < ε := by linarith + · simpa + have t₁ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.re := by + apply ContinuousOn.intervalIntegrable + apply ContinuousOn.comp + apply hf + fun_prop + intro x _ + simpa + rw [← intervalIntegral.integral_sub t₀ t₁] + + have t₂ : IntervalIntegrable (fun x_1 => f { re := y.re, im := x_1 }) MeasureTheory.volume 0 y.im := by + apply ContinuousOn.intervalIntegrable + apply ContinuousOn.comp + exact hf + have : (Complex.mk y.re) = (fun x => Complex.I • Complex.ofRealCLM x + { re := y.re, im := 0 }) := by + funext x + apply Complex.ext + rw [Complex.add_re] + simp + simp + rw [this] + apply ContinuousOn.add + apply Continuous.continuousOn + continuity + fun_prop + intro x hx + apply h₂ε.2 + constructor + · simp + calc |y.re| + _ ≤ Complex.abs y := by exact Complex.abs_re_le_abs y + _ < ε / 4 := by simp at hy; assumption + _ < ε := by linarith + · simp + calc |x| + _ ≤ |y.im| := by apply intervalComputation_uIcc hx + _ ≤ Complex.abs y := by exact Complex.abs_im_le_abs y + _ < ε / 4 := by simp at hy; assumption + _ < ε := by linarith + have t₃ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.im := by + apply ContinuousOn.intervalIntegrable + apply ContinuousOn.comp + exact hf + fun_prop + intro x _ + apply h₂ε.2 + simp + constructor + · simpa + · simpa + rw [← intervalIntegral.integral_sub t₂ t₃] + have h₁y : |y.re| < ε / 4 := by calc |y.re| _ ≤ Complex.abs y := by apply Complex.abs_re_le_abs @@ -383,12 +262,11 @@ theorem primitive_fderivAtBasepointZero _ < ε / 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 + constructor + · simp + linarith + · simp + exact h₁ε 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 @@ -401,13 +279,11 @@ theorem primitive_fderivAtBasepointZero 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 + constructor + · simp + linarith + · simp + 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 @@ -488,14 +364,21 @@ theorem primitive_translation theorem primitive_hasDerivAtBasepoint {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} - (hf : Continuous f) - (z₀ : ℂ) : + {R : ℝ} + (z₀ : ℂ) + (hR : 0 < R) + (hf : ContinuousOn f (Metric.ball z₀ R)) : 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 + have hg : ContinuousOn g (Metric.ball 0 R) := by + apply ContinuousOn.comp + fun_prop + fun_prop + intro x hx + simp + simp at hx + assumption let B := primitive_translation g z₀ z₀ simp at B @@ -505,8 +388,7 @@ theorem primitive_hasDerivAtBasepoint simp rw [this] at B rw [B] - have : f z₀ = (1 : ℂ) • (f z₀) := by - exact (MulAction.one_smul (f z₀)).symm + have : f z₀ = (1 : ℂ) • (f z₀) := (MulAction.one_smul (f z₀)).symm conv => arg 2 rw [this] @@ -515,7 +397,7 @@ theorem primitive_hasDerivAtBasepoint simp have : g 0 = f z₀ := by simp [g] rw [← this] - exact A + exact primitive_fderivAtBasepointZero hR hg apply HasDerivAt.sub_const have : (fun (x : ℂ) ↦ x) = id := by funext x @@ -524,143 +406,441 @@ 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) - (hf : Differentiable ℂ f) - (z₀ z₁ : ℂ) : - primitive z₀ f = fun z ↦ (primitive z₁ f) z + (primitive z₀ f z₁) := by - funext z + {f : ℂ → E} + {z₀ : ℂ} + {rx ry : ℝ} + (hf : DifferentiableOn ℂ f (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)) + (hry : 0 < 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 + let A := hz₁.1 + simp at A + dsimp [εx] + rw [dist_comm] + simpa + let εy := ry - dist z₀.im z₁.im + have hεy : εy > 0 := by + let A := hz₁.2 + simp at A + dsimp [εy] + rw [dist_comm] + simpa + + use εx + use hεx + use εy + use hεy + + intro z hz + 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 [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₀.re rx ×ℂ Metric.ball z₀.im ry) + intro w hw + simp + apply Complex.mem_reProdIm.mpr + constructor + · simp + 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 + _ < rx := by apply Metric.mem_ball.mp (Complex.mem_reProdIm.1 hz₁).1 + · simpa + + -- 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₀.re rx ×ℂ Metric.ball z₀.im ry) + intro w hw + simp + constructor + · simp + 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_iff_right (dist z₁.re z₀.re)).mpr + rw [Set.uIcc_comm] at hw + exact Real.dist_right_le_of_mem_uIcc hw + _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by + apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr + apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1 + _ = rx := by + rw [dist_comm] + simp + · simpa 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 + + -- 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₀.re rx ×ℂ Metric.ball z₀.im ry) + intro w hw + constructor + · simp + calc dist z.re z₀.re + _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle z.re z₁.re z₀.re + _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by + apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr + apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1 + _ = rx := by + rw [dist_comm] + simp + · simp + calc dist w z₀.im + _ ≤ dist z₁.im z₀.im := by rw [Set.uIcc_comm] at hw; exact Real.dist_right_le_of_mem_uIcc hw + _ < ry := by + rw [← Metric.mem_ball] + exact hz₁.2 + + -- 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₀.re rx ×ℂ Metric.ball z₀.im ry) + intro w hw + constructor + · simp + calc dist z.re z₀.re + _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle z.re z₁.re z₀.re + _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by + apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr + apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1 + _ = rx := by + rw [dist_comm] + simp + · simp + calc dist w z₀.im + _ ≤ dist w z₁.im + dist z₁.im z₀.im := by exact dist_triangle w z₁.im z₀.im + _ ≤ dist z.im z₁.im + dist z₁.im z₀.im := by + apply (add_le_add_iff_right (dist z₁.im z₀.im)).mpr + rw [Set.uIcc_comm] at hw + exact Real.dist_right_le_of_mem_uIcc hw + _ < (ry - dist z₀.im z₁.im) + dist z₁.im z₀.im := by + apply (add_lt_add_iff_right (dist z₁.im z₀.im)).mpr + apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).2 + _ = ry := by + rw [dist_comm] + simp rw [this] + simp - let A := integral_divergence₅ f hf ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ - simp at A - - have {a b c d : E} : (b + a) + (c + d) = (a + c) + (b + d) := by + 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] - rw [A] + + + have H' : DifferentiableOn ℂ f (Set.uIcc z₁.re z.re ×ℂ Set.uIcc z₀.im z₁.im) := by + apply DifferentiableOn.mono hf + intro x hx + constructor + · simp + calc dist x.re z₀.re + _ ≤ dist x.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle x.re z₁.re z₀.re + _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by + apply (add_le_add_iff_right (dist z₁.re z₀.re)).mpr + rw [Set.uIcc_comm] at hx + apply Real.dist_right_le_of_mem_uIcc (Complex.mem_reProdIm.1 hx).1 + _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by + apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr + apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1 + _ = rx := by + rw [dist_comm] + simp + · simp + calc dist x.im z₀.im + _ ≤ dist z₀.im z₁.im := by rw [dist_comm]; exact Real.dist_left_le_of_mem_uIcc (Complex.mem_reProdIm.1 hx).2 + _ < ry := by + rw [dist_comm] + exact Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz₁).2 + + 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 + · 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} + {z₀ z₁ : ℂ} + {R : ℝ} + (hf : DifferentiableOn ℂ f (Metric.ball z₀ R)) + (hz₁ : z₁ ∈ Metric.ball z₀ R) + : + primitive z₀ f =ᶠ[nhds z₁] fun z ↦ (primitive z₁ f z) + (primitive z₀ f z₁) := by + + let d := fun ε ↦ √((dist z₁.re z₀.re + ε) ^ 2 + (dist z₁.im z₀.im + ε) ^ 2) + have h₀d : Continuous d := by continuity + have h₁d : ∀ ε, 0 ≤ d ε := fun ε ↦ Real.sqrt_nonneg ((dist z₁.re z₀.re + ε) ^ 2 + (dist z₁.im z₀.im + ε) ^ 2) + + obtain ⟨ε, h₀ε, h₁ε⟩ : ∃ ε > 0, d ε < R := by + let Omega := d⁻¹' Metric.ball 0 R + + have lem₀Ω : IsOpen Omega := IsOpen.preimage h₀d Metric.isOpen_ball + have lem₁Ω : 0 ∈ Omega := by + dsimp [Omega, d]; simp + have : dist z₁.re z₀.re = |z₁.re - z₀.re| := by exact rfl + rw [this] + have : dist z₁.im z₀.im = |z₁.im - z₀.im| := by exact rfl + rw [this] + simp + rw [← Complex.dist_eq_re_im]; simp + exact hz₁ + obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 lem₀Ω 0 lem₁Ω + + let ε' := (2 : ℝ)⁻¹ * ε + + have h₀ε' : ε' ∈ Omega := by + apply h₂ε + dsimp [ε']; simp + have : |ε| = ε := by apply abs_of_pos h₁ε + rw [this] + apply (inv_mul_lt_iff zero_lt_two).mpr + linarith + have h₁ε' : 0 < ε' := by + apply Real.mul_pos _ h₁ε + apply inv_pos.mpr + exact zero_lt_two + + use ε' + + constructor + · exact h₁ε' + · dsimp [Omega] at h₀ε'; simp at h₀ε' + rwa [abs_of_nonneg (h₁d ε')] at h₀ε' + + let rx := dist z₁.re z₀.re + ε + let ry := dist z₁.im z₀.im + ε + + 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 + rw [Complex.dist_eq_re_im] + + have t₀ : dist x.re z₀.re < rx := Metric.mem_ball.mp hx.1 + have t₁ : dist x.im z₀.im < ry := Metric.mem_ball.mp hx.2 + have t₂ : √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) < √( rx ^ 2 + ry ^ 2) := by + rw [Real.sqrt_lt_sqrt_iff] + apply add_lt_add + · rw [sq_lt_sq] + dsimp [dist] at t₀ + nth_rw 2 [abs_of_nonneg] + assumption + apply add_nonneg dist_nonneg (le_of_lt h₀ε) + · rw [sq_lt_sq] + dsimp [dist] at t₁ + nth_rw 2 [abs_of_nonneg] + assumption + apply add_nonneg dist_nonneg (le_of_lt h₀ε) + apply add_nonneg + exact sq_nonneg (x.re - z₀.re) + exact sq_nonneg (x.im - z₀.im) + + calc √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) + _ < √( rx ^ 2 + ry ^ 2) := by + exact t₂ + _ = d ε := by dsimp [d, rx, ry] + _ < R := by exact h₁ε + + have h'z₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by + dsimp [rx, ry] + constructor + · simp; exact h₀ε + · 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} - (hf : Differentiable ℂ f) - (z₀ z : ℂ) : + {z₀ z : ℂ} + {R : ℝ} + (hf : DifferentiableOn ℂ f (Metric.ball z₀ R)) + (hz : z ∈ Metric.ball z₀ R) : HasDerivAt (primitive z₀ f) (f z) z := by - rw [primitive_additivity f hf z₀ z] + + let A := primitive_additivity' hf hz + rw [Filter.EventuallyEq.hasDerivAt_iff A] rw [← add_zero (f z)] apply HasDerivAt.add + + let R' := R - dist z z₀ + have h₀R' : 0 < R' := by + dsimp [R'] + simp + exact hz + have h₁R' : Metric.ball z R' ⊆ Metric.ball z₀ R := by + intro x hx + simp + calc dist x z₀ + _ ≤ dist x z + dist z z₀ := dist_triangle x z z₀ + _ < R' + dist z z₀ := by + refine add_lt_add_right ?bc (dist z z₀) + exact hx + _ = R := by + dsimp [R'] + simp + apply primitive_hasDerivAtBasepoint - exact hf.continuous + exact h₀R' + apply ContinuousOn.mono hf.continuousOn h₁R' apply hasDerivAt_const -theorem primitive_differentiable +theorem primitive_differentiableOn {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 + {z₀ : ℂ} + {R : ℝ} + (hf : DifferentiableOn ℂ f (Metric.ball z₀ R)) + : + DifferentiableOn ℂ (primitive z₀ f) (Metric.ball z₀ R) := by + intro z hz + apply DifferentiableAt.differentiableWithinAt + exact (primitive_hasDerivAt hf hz).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 + (z₀ : ℂ) + (R : ℝ) + (hf : DifferentiableOn ℂ f (Metric.ball z₀ R)) + : + ∀ z ∈ Metric.ball z₀ R, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ℂ ℂ).flip (f z)) z := by + intro z hz rw [hasFDerivAt_iff_hasDerivAt] - simp - exact primitive_hasDerivAt hf z₀ z + simp + apply primitive_hasDerivAt hf hz theorem primitive_hasFderivAt' {f : ℂ → ℂ} - (hf : Differentiable ℂ f) - (z₀ : ℂ) : - ∀ z, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul ℂ ℂ (f z)) z := by - intro z + {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 z₀ z + simp + exact primitive_hasDerivAt hf hz 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 + {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 + intro z hz apply HasFDerivAt.fderiv - exact primitive_hasFderivAt hf z₀ z + exact primitive_hasFderivAt z₀ R hf z hz theorem primitive_fderiv' {f : ℂ → ℂ} - (hf : Differentiable ℂ f) - (z₀ : ℂ) : - ∀ z, (fderiv ℂ (primitive z₀ f) z) = ContinuousLinearMap.lsmul ℂ ℂ (f z) := by - intro z + {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₀ z - + exact primitive_hasFderivAt' hf z hz diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean deleted file mode 100644 index 640ee43..0000000 --- a/Nevanlinna/holomorphic_primitive2.lean +++ /dev/null @@ -1,846 +0,0 @@ -import Mathlib.Analysis.Complex.TaylorSeries -import Mathlib.Data.ENNReal.Basic - -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} - {R : ℝ} - (hR : 0 < R) - (hf : ContinuousOn f (Metric.ball 0 R)) : - 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] - - obtain ⟨s, h₁s, h₂s⟩ : ∃ s ⊆ f⁻¹' Metric.ball (f 0) (c / (4 : ℝ)), IsOpen s ∧ 0 ∈ s := by - apply eventually_nhds_iff.mp - apply continuousAt_def.1 - apply Continuous.continuousAt - fun_prop - - apply continuousAt_def.1 - apply hf.continuousAt - exact Metric.ball_mem_nhds 0 hR - apply Metric.ball_mem_nhds (f 0) - simpa - - obtain ⟨ε, h₁ε, h₂ε⟩ : ∃ ε > 0, (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ s ∧ (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ Metric.ball 0 R := by - obtain ⟨ε', h₁ε', h₂ε'⟩ : ∃ ε' > 0, Metric.ball 0 ε' ⊆ s ∩ Metric.ball 0 R := by - apply Metric.mem_nhds_iff.mp - apply IsOpen.mem_nhds - apply IsOpen.inter - exact h₂s.1 - exact Metric.isOpen_ball - constructor - · exact h₂s.2 - · simpa - - use (2 : ℝ)⁻¹ * ε' - - constructor - · simpa - · constructor - · intro x hx - apply (h₂ε' _).1 - simp - calc Complex.abs x - _ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x - _ < (2 : ℝ)⁻¹ * ε' + |x.im| := by - apply (add_lt_add_iff_right |x.im|).mpr - have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1 - simp at this - exact this - _ < (2 : ℝ)⁻¹ * ε' + (2 : ℝ)⁻¹ * ε' := by - apply (add_lt_add_iff_left ((2 : ℝ)⁻¹ * ε')).mpr - have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2 - simp at this - exact this - _ = ε' := by - rw [← add_mul] - abel_nf - simp - · intro x hx - apply (h₂ε' _).2 - simp - calc Complex.abs x - _ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x - _ < (2 : ℝ)⁻¹ * ε' + |x.im| := by - apply (add_lt_add_iff_right |x.im|).mpr - have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1 - simp at this - exact this - _ < (2 : ℝ)⁻¹ * ε' + (2 : ℝ)⁻¹ * ε' := by - apply (add_lt_add_iff_left ((2 : ℝ)⁻¹ * ε')).mpr - have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2 - simp at this - exact this - _ = ε' := by - rw [← add_mul] - abel_nf - simp - - have h₃ε : ∀ y ∈ (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε), ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by - intro y hy - apply mem_ball_iff_norm.mp - apply h₁s - exact h₂ε.1 hy - - - have intervalComputation_uIcc {x' y' : ℝ} (h : x' ∈ Set.uIcc 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 - rwa [abs_of_nonneg A, abs_of_nonneg hy] - · simp [hy] at A - simp [hy] at B - rw [abs_of_nonpos hy] - rw [abs_of_nonpos] - linarith [h.1] - exact B - - - rw [Filter.eventually_iff_exists_mem] - use Metric.ball 0 (ε / (4 : ℝ)) - - constructor - · apply Metric.ball_mem_nhds 0 - linarith - · intro y hy - - have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by - abel - rw [this] - rw [← smul_sub] - - - have t₀ : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 y.re := by - apply ContinuousOn.intervalIntegrable - apply ContinuousOn.comp - exact hf - have : (fun x => ({ re := x, im := 0 } : ℂ)) = Complex.ofRealLI := by rfl - rw [this] - apply Continuous.continuousOn - continuity - intro x hx - apply h₂ε.2 - simp - constructor - · simp - calc |x| - _ ≤ |y.re| := by apply intervalComputation_uIcc hx - _ ≤ Complex.abs y := by exact Complex.abs_re_le_abs y - _ < ε / 4 := by simp at hy; assumption - _ < ε := by linarith - · simpa - have t₁ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.re := by - apply ContinuousOn.intervalIntegrable - apply ContinuousOn.comp - apply hf - fun_prop - intro x _ - simpa - rw [← intervalIntegral.integral_sub t₀ t₁] - - have t₂ : IntervalIntegrable (fun x_1 => f { re := y.re, im := x_1 }) MeasureTheory.volume 0 y.im := by - apply ContinuousOn.intervalIntegrable - apply ContinuousOn.comp - exact hf - have : (Complex.mk y.re) = (fun x => Complex.I • Complex.ofRealCLM x + { re := y.re, im := 0 }) := by - funext x - apply Complex.ext - rw [Complex.add_re] - simp - simp - rw [this] - apply ContinuousOn.add - apply Continuous.continuousOn - continuity - fun_prop - intro x hx - apply h₂ε.2 - constructor - · simp - calc |y.re| - _ ≤ Complex.abs y := by exact Complex.abs_re_le_abs y - _ < ε / 4 := by simp at hy; assumption - _ < ε := by linarith - · simp - calc |x| - _ ≤ |y.im| := by apply intervalComputation_uIcc hx - _ ≤ Complex.abs y := by exact Complex.abs_im_le_abs y - _ < ε / 4 := by simp at hy; assumption - _ < ε := by linarith - have t₃ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.im := by - apply ContinuousOn.intervalIntegrable - apply ContinuousOn.comp - exact hf - fun_prop - intro x _ - apply h₂ε.2 - simp - constructor - · simpa - · simpa - rw [← intervalIntegral.integral_sub t₂ t₃] - - 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 } - constructor - · simp - linarith - · simp - exact h₁ε - - 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 } - constructor - · simp - linarith - · simp - 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} - {R : ℝ} - (z₀ : ℂ) - (hR : 0 < R) - (hf : ContinuousOn f (Metric.ball z₀ R)) : - HasDerivAt (primitive z₀ f) (f z₀) z₀ := by - - let g := f ∘ fun z ↦ z + z₀ - have hg : ContinuousOn g (Metric.ball 0 R) := by - apply ContinuousOn.comp - fun_prop - fun_prop - intro x hx - simp - simp at hx - assumption - - 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₀) := (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 primitive_fderivAtBasepointZero hR hg - apply HasDerivAt.sub_const - have : (fun (x : ℂ) ↦ x) = id := by - funext x - simp - rw [this] - exact hasDerivAt_id z₀ - - -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)) - (hry : 0 < 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 - let A := hz₁.1 - simp at A - dsimp [εx] - rw [dist_comm] - simpa - let εy := ry - dist z₀.im z₁.im - have hεy : εy > 0 := by - let A := hz₁.2 - simp at A - dsimp [εy] - rw [dist_comm] - simpa - - use εx - use hεx - use εy - use hεy - - intro z hz - - 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] - - -- 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₀.re rx ×ℂ Metric.ball z₀.im ry) - intro w hw - simp - apply Complex.mem_reProdIm.mpr - constructor - · simp - 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 - _ < rx := by apply Metric.mem_ball.mp (Complex.mem_reProdIm.1 hz₁).1 - · simpa - - -- 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₀.re rx ×ℂ Metric.ball z₀.im ry) - intro w hw - simp - constructor - · simp - 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_iff_right (dist z₁.re z₀.re)).mpr - rw [Set.uIcc_comm] at hw - exact Real.dist_right_le_of_mem_uIcc hw - _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by - apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr - apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1 - _ = rx := by - rw [dist_comm] - simp - · simpa - 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₀.re rx ×ℂ Metric.ball z₀.im ry) - intro w hw - constructor - · simp - calc dist z.re z₀.re - _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle z.re z₁.re z₀.re - _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by - apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr - apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1 - _ = rx := by - rw [dist_comm] - simp - · simp - calc dist w z₀.im - _ ≤ dist z₁.im z₀.im := by rw [Set.uIcc_comm] at hw; exact Real.dist_right_le_of_mem_uIcc hw - _ < ry := by - rw [← Metric.mem_ball] - exact hz₁.2 - - -- 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₀.re rx ×ℂ Metric.ball z₀.im ry) - intro w hw - constructor - · simp - calc dist z.re z₀.re - _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle z.re z₁.re z₀.re - _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by - apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr - apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1 - _ = rx := by - rw [dist_comm] - simp - · simp - calc dist w z₀.im - _ ≤ dist w z₁.im + dist z₁.im z₀.im := by exact dist_triangle w z₁.im z₀.im - _ ≤ dist z.im z₁.im + dist z₁.im z₀.im := by - apply (add_le_add_iff_right (dist z₁.im z₀.im)).mpr - rw [Set.uIcc_comm] at hw - exact Real.dist_right_le_of_mem_uIcc hw - _ < (ry - dist z₀.im z₁.im) + dist z₁.im z₀.im := by - apply (add_lt_add_iff_right (dist z₁.im z₀.im)).mpr - apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).2 - _ = ry := by - rw [dist_comm] - simp - 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] - - - have H' : DifferentiableOn ℂ f (Set.uIcc z₁.re z.re ×ℂ Set.uIcc z₀.im z₁.im) := by - apply DifferentiableOn.mono hf - intro x hx - constructor - · simp - calc dist x.re z₀.re - _ ≤ dist x.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle x.re z₁.re z₀.re - _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by - apply (add_le_add_iff_right (dist z₁.re z₀.re)).mpr - rw [Set.uIcc_comm] at hx - apply Real.dist_right_le_of_mem_uIcc (Complex.mem_reProdIm.1 hx).1 - _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by - apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr - apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1 - _ = rx := by - rw [dist_comm] - simp - · simp - calc dist x.im z₀.im - _ ≤ dist z₀.im z₁.im := by rw [dist_comm]; exact Real.dist_left_le_of_mem_uIcc (Complex.mem_reProdIm.1 hx).2 - _ < ry := by - rw [dist_comm] - exact Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz₁).2 - - 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 - · 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} - {z₀ z₁ : ℂ} - {R : ℝ} - (hf : DifferentiableOn ℂ f (Metric.ball z₀ R)) - (hz₁ : z₁ ∈ Metric.ball z₀ R) - : - primitive z₀ f =ᶠ[nhds z₁] fun z ↦ (primitive z₁ f z) + (primitive z₀ f z₁) := by - - let d := fun ε ↦ √((dist z₁.re z₀.re + ε) ^ 2 + (dist z₁.im z₀.im + ε) ^ 2) - have h₀d : Continuous d := by continuity - have h₁d : ∀ ε, 0 ≤ d ε := fun ε ↦ Real.sqrt_nonneg ((dist z₁.re z₀.re + ε) ^ 2 + (dist z₁.im z₀.im + ε) ^ 2) - - obtain ⟨ε, h₀ε, h₁ε⟩ : ∃ ε > 0, d ε < R := by - let Omega := d⁻¹' Metric.ball 0 R - - have lem₀Ω : IsOpen Omega := IsOpen.preimage h₀d Metric.isOpen_ball - have lem₁Ω : 0 ∈ Omega := by - dsimp [Omega, d]; simp - have : dist z₁.re z₀.re = |z₁.re - z₀.re| := by exact rfl - rw [this] - have : dist z₁.im z₀.im = |z₁.im - z₀.im| := by exact rfl - rw [this] - simp - rw [← Complex.dist_eq_re_im]; simp - exact hz₁ - obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 lem₀Ω 0 lem₁Ω - - let ε' := (2 : ℝ)⁻¹ * ε - - have h₀ε' : ε' ∈ Omega := by - apply h₂ε - dsimp [ε']; simp - have : |ε| = ε := by apply abs_of_pos h₁ε - rw [this] - apply (inv_mul_lt_iff zero_lt_two).mpr - linarith - have h₁ε' : 0 < ε' := by - apply Real.mul_pos _ h₁ε - apply inv_pos.mpr - exact zero_lt_two - - use ε' - - constructor - · exact h₁ε' - · dsimp [Omega] at h₀ε'; simp at h₀ε' - rwa [abs_of_nonneg (h₁d ε')] at h₀ε' - - let rx := dist z₁.re z₀.re + ε - let ry := dist z₁.im z₀.im + ε - - 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 - rw [Complex.dist_eq_re_im] - - have t₀ : dist x.re z₀.re < rx := Metric.mem_ball.mp hx.1 - have t₁ : dist x.im z₀.im < ry := Metric.mem_ball.mp hx.2 - have t₂ : √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) < √( rx ^ 2 + ry ^ 2) := by - rw [Real.sqrt_lt_sqrt_iff] - apply add_lt_add - · rw [sq_lt_sq] - dsimp [dist] at t₀ - nth_rw 2 [abs_of_nonneg] - assumption - apply add_nonneg dist_nonneg (le_of_lt h₀ε) - · rw [sq_lt_sq] - dsimp [dist] at t₁ - nth_rw 2 [abs_of_nonneg] - assumption - apply add_nonneg dist_nonneg (le_of_lt h₀ε) - apply add_nonneg - exact sq_nonneg (x.re - z₀.re) - exact sq_nonneg (x.im - z₀.im) - - calc √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) - _ < √( rx ^ 2 + ry ^ 2) := by - exact t₂ - _ = d ε := by dsimp [d, rx, ry] - _ < R := by exact h₁ε - - have h'z₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by - dsimp [rx, ry] - constructor - · simp; exact h₀ε - · 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 : ℝ} - (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 - rw [Filter.EventuallyEq.hasDerivAt_iff A] - rw [← add_zero (f z)] - apply HasDerivAt.add - - let R' := R - dist z z₀ - have h₀R' : 0 < R' := by - dsimp [R'] - simp - exact hz - have h₁R' : Metric.ball z R' ⊆ Metric.ball z₀ R := by - intro x hx - simp - calc dist x z₀ - _ ≤ dist x z + dist z z₀ := dist_triangle x z z₀ - _ < R' + dist z z₀ := by - refine add_lt_add_right ?bc (dist z z₀) - exact hx - _ = R := by - dsimp [R'] - simp - - apply primitive_hasDerivAtBasepoint - exact h₀R' - apply ContinuousOn.mono hf.continuousOn h₁R' - apply hasDerivAt_const - - -theorem primitive_differentiableOn - {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] - {f : ℂ → E} - {z₀ : ℂ} - {R : ℝ} - (hf : DifferentiableOn ℂ f (Metric.ball z₀ R)) - : - DifferentiableOn ℂ (primitive z₀ f) (Metric.ball z₀ R) := by - intro z hz - apply DifferentiableAt.differentiableWithinAt - exact (primitive_hasDerivAt hf hz).differentiableAt - - -theorem primitive_hasFderivAt - {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] - {f : ℂ → E} - (z₀ : ℂ) - (R : ℝ) - (hf : DifferentiableOn ℂ f (Metric.ball z₀ R)) - : - ∀ z ∈ Metric.ball z₀ R, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ℂ ℂ).flip (f z)) z := by - intro z hz - rw [hasFDerivAt_iff_hasDerivAt] - simp - apply primitive_hasDerivAt hf hz - - -theorem primitive_hasFderivAt' - {f : ℂ → ℂ} - {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 - - -theorem primitive_fderiv - {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] - {f : ℂ → E} - {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 - intro z hz - apply HasFDerivAt.fderiv - exact primitive_hasFderivAt z₀ R hf z hz - - -theorem primitive_fderiv' - {f : ℂ → ℂ} - {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 diff --git a/Nevanlinna/junk/holomorphic_primitive.lean b/Nevanlinna/junk/holomorphic_primitive.lean new file mode 100644 index 0000000..9b393cc --- /dev/null +++ b/Nevanlinna/junk/holomorphic_primitive.lean @@ -0,0 +1,666 @@ +import Mathlib.Analysis.Complex.TaylorSeries +import Mathlib.Analysis.SpecialFunctions.Integrals +import Mathlib.MeasureTheory.Integral.DivergenceTheorem +import Mathlib.MeasureTheory.Integral.IntervalIntegral +import Mathlib.MeasureTheory.Function.LocallyIntegrable +import Nevanlinna.partialDeriv +import Nevanlinna.cauchyRiemann + +/- +noncomputable def partialDeriv + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] : E → (E → F) → (E → F) := + fun v ↦ (fun f ↦ (fun w ↦ fderiv ℝ f w v)) + + +theorem partialDeriv_compContLinAt + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] + {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] + {f : E → F} + {l : F →L[ℝ] G} + {v : E} + {x : E} + (h : DifferentiableAt ℝ f x) : + (partialDeriv v (l ∘ f)) x = (l ∘ partialDeriv v f) x:= by + unfold partialDeriv + rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h] + simp + + +theorem partialDeriv_compCLE + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] + {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] + {f : E → F} + {l : F ≃L[ℝ] G} {v : E} : partialDeriv v (l ∘ f) = l ∘ partialDeriv v f := by + funext x + by_cases hyp : DifferentiableAt ℝ f x + · let lCLM : F →L[ℝ] G := l + suffices shyp : partialDeriv v (lCLM ∘ f) x = (lCLM ∘ partialDeriv v f) x from by tauto + apply partialDeriv_compContLinAt + exact hyp + · unfold partialDeriv + rw [fderiv_zero_of_not_differentiableAt] + simp + rw [fderiv_zero_of_not_differentiableAt] + simp + exact hyp + rw [ContinuousLinearEquiv.comp_differentiableAt_iff] + exact hyp + +theorem partialDeriv_smul'₂ + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] + {f : E → F} {a : ℂ} {v : E} : + partialDeriv v (a • f) = a • partialDeriv v f := by + + funext w + by_cases ha : a = 0 + · unfold partialDeriv + have : a • f = fun y ↦ a • f y := by rfl + rw [this, ha] + simp + · -- Now a is not zero. We present scalar multiplication with a as a continuous linear equivalence. + let smulCLM : F ≃L[ℝ] F := + { + toFun := fun x ↦ a • x + map_add' := fun x y => DistribSMul.smul_add a x y + map_smul' := fun m x => (smul_comm ((RingHom.id ℝ) m) a x).symm + invFun := fun x ↦ a⁻¹ • x + left_inv := by + intro x + simp + rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel ha, one_smul] + right_inv := by + intro x + simp + rw [← smul_assoc, smul_eq_mul, mul_inv_cancel ha, one_smul] + continuous_toFun := continuous_const_smul a + continuous_invFun := continuous_const_smul a⁻¹ + } + + have : a • f = smulCLM ∘ f := by tauto + rw [this] + rw [partialDeriv_compCLE] + tauto + +theorem CauchyRiemann₄ + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] + {f : ℂ → F} : + (Differentiable ℂ f) → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by + intro h + unfold partialDeriv + + conv => + left + intro w + rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)] + simp + rw [← mul_one Complex.I] + rw [← smul_eq_mul] + conv => + right + right + intro w + rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)] + funext w + simp +-/ + + +theorem MeasureTheory.integral2_divergence₃ + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] + (f g : ℝ × ℝ → E) + (h₁f : ContDiff ℝ 1 f) + (h₁g : ContDiff ℝ 1 g) + (a₁ : ℝ) + (a₂ : ℝ) + (b₁ : ℝ) + (b₂ : ℝ) : + ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, ((fderiv ℝ f) (x, y)) (1, 0) + ((fderiv ℝ g) (x, y)) (0, 1) = (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) - ∫ (y : ℝ) in a₂..b₂, f (a₁, y) := by + + apply integral2_divergence_prod_of_hasFDerivWithinAt_off_countable f g (fderiv ℝ f) (fderiv ℝ g) a₁ a₂ b₁ b₂ ∅ + exact Set.countable_empty + -- ContinuousOn f (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂) + exact h₁f.continuous.continuousOn + -- + exact h₁g.continuous.continuousOn + -- + rw [Set.diff_empty] + intro x _ + exact DifferentiableAt.hasFDerivAt ((h₁f.differentiable le_rfl) x) + -- + rw [Set.diff_empty] + intro y _ + exact DifferentiableAt.hasFDerivAt ((h₁g.differentiable le_rfl) y) + -- + apply ContinuousOn.integrableOn_compact + apply IsCompact.prod + exact isCompact_uIcc + exact isCompact_uIcc + apply ContinuousOn.add + apply Continuous.continuousOn + exact Continuous.clm_apply (ContDiff.continuous_fderiv h₁f le_rfl) continuous_const + apply Continuous.continuousOn + exact Continuous.clm_apply (ContDiff.continuous_fderiv h₁g le_rfl) continuous_const + + +theorem integral_divergence₄ + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] + (f g : ℂ → E) + (h₁f : ContDiff ℝ 1 f) + (h₁g : ContDiff ℝ 1 g) + (a₁ : ℝ) + (a₂ : ℝ) + (b₁ : ℝ) + (b₂ : ℝ) : + ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, ((fderiv ℝ f) ⟨x, y⟩ ) 1 + ((fderiv ℝ g) ⟨x, y⟩) Complex.I = (((∫ (x : ℝ) in a₁..b₁, g ⟨x, b₂⟩) - ∫ (x : ℝ) in a₁..b₁, g ⟨x, a₂⟩) + ∫ (y : ℝ) in a₂..b₂, f ⟨b₁, y⟩) - ∫ (y : ℝ) in a₂..b₂, f ⟨a₁, y⟩ := by + + let fr : ℝ × ℝ → E := f ∘ Complex.equivRealProdCLM.symm + let gr : ℝ × ℝ → E := g ∘ Complex.equivRealProdCLM.symm + + have sfr {x y : ℝ} : f { re := x, im := y } = fr (x, y) := by exact rfl + have sgr {x y : ℝ} : g { re := x, im := y } = gr (x, y) := by exact rfl + repeat (conv in f { re := _, im := _ } => rw [sfr]) + repeat (conv in g { re := _, im := _ } => rw [sgr]) + + have sfr' {x y : ℝ} {z : ℂ} : (fderiv ℝ f { re := x, im := y }) z = fderiv ℝ fr (x, y) (Complex.equivRealProdCLM z) := by + rw [fderiv.comp] + rw [Complex.equivRealProdCLM.symm.fderiv] + tauto + apply Differentiable.differentiableAt + exact h₁f.differentiable le_rfl + exact Complex.equivRealProdCLM.symm.differentiableAt + conv in ⇑(fderiv ℝ f { re := _, im := _ }) _ => rw [sfr'] + + have sgr' {x y : ℝ} {z : ℂ} : (fderiv ℝ g { re := x, im := y }) z = fderiv ℝ gr (x, y) (Complex.equivRealProdCLM z) := by + rw [fderiv.comp] + rw [Complex.equivRealProdCLM.symm.fderiv] + tauto + apply Differentiable.differentiableAt + exact h₁g.differentiable le_rfl + exact Complex.equivRealProdCLM.symm.differentiableAt + conv in ⇑(fderiv ℝ g { re := _, im := _ }) _ => rw [sgr'] + + apply MeasureTheory.integral2_divergence₃ fr gr _ _ a₁ a₂ b₁ b₂ + -- ContDiff ℝ 1 fr + exact (ContinuousLinearEquiv.contDiff_comp_iff (ContinuousLinearEquiv.symm Complex.equivRealProdCLM)).mpr h₁f + -- ContDiff ℝ 1 gr + exact (ContinuousLinearEquiv.contDiff_comp_iff (ContinuousLinearEquiv.symm Complex.equivRealProdCLM)).mpr h₁g + + +theorem integral_divergence₅ + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] + (F : ℂ → E) + (hF : Differentiable ℂ F) + (lowerLeft upperRight : ℂ) : + (∫ (x : ℝ) in lowerLeft.re..upperRight.re, F ⟨x, lowerLeft.im⟩) + Complex.I • ∫ (x : ℝ) in lowerLeft.im..upperRight.im, F ⟨upperRight.re, x⟩ = + (∫ (x : ℝ) in lowerLeft.re..upperRight.re, F ⟨x, upperRight.im⟩) + Complex.I • ∫ (x : ℝ) in lowerLeft.im..upperRight.im, F ⟨lowerLeft.re, x⟩ := by + + let h₁f : ContDiff ℝ 1 F := (hF.contDiff : ContDiff ℂ 1 F).restrict_scalars ℝ + + let h₁g : ContDiff ℝ 1 (-Complex.I • F) := by + have : -Complex.I • F = fun x ↦ -Complex.I • F x := by rfl + rw [this] + apply ContDiff.comp + exact contDiff_const_smul _ + exact h₁f + + let A := integral_divergence₄ (-Complex.I • F) F h₁g h₁f lowerLeft.re upperRight.im upperRight.re lowerLeft.im + have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv ℝ Complex.I F z := by rfl + conv at A in (fderiv ℝ F _) _ => rw [this] + have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv ℝ 1 (-Complex.I • F) z := by rfl + conv at A in (fderiv ℝ (-Complex.I • F) _) _ => rw [this] + conv at A => + left + arg 1 + intro x + arg 1 + intro y + rw [CauchyRiemann₄ hF] + rw [partialDeriv_smul'₂] + simp + simp at A + + have {t₁ t₂ t₃ t₄ : E} : 0 = (t₁ - t₂) + t₃ + t₄ → t₁ + t₃ = t₂ - t₄ := by + intro hyp + calc + t₁ + t₃ = t₁ + t₃ - 0 := by rw [sub_zero (t₁ + t₃)] + _ = t₁ + t₃ - (t₁ - t₂ + t₃ + t₄) := by rw [hyp] + _ = t₂ - t₄ := by abel + let B := this A + repeat + rw [intervalIntegral.integral_symm lowerLeft.im upperRight.im] at B + simp at B + exact B + + +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₁ : ℂ) : + primitive z₀ f = fun z ↦ (primitive z₁ f) z + (primitive z₀ f z₁) := 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 + + let A := integral_divergence₅ f hf ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ + simp at A + + have {a b c d : E} : (b + a) + (c + d) = (a + c) + (b + d) := by + abel + rw [this] + rw [A] + 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 +