667 lines
21 KiB
Plaintext
667 lines
21 KiB
Plaintext
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
|
||
|