Update holomorphic.primitive.lean
This commit is contained in:
Stefan Kebekus
parent
7a281ff514
commit
0a68e3a344
|
|
@ -4,7 +4,104 @@ import Mathlib.MeasureTheory.Integral.DivergenceTheorem
|
||||||
import Mathlib.MeasureTheory.Integral.IntervalIntegral
|
import Mathlib.MeasureTheory.Integral.IntervalIntegral
|
||||||
import Mathlib.MeasureTheory.Function.LocallyIntegrable
|
import Mathlib.MeasureTheory.Function.LocallyIntegrable
|
||||||
|
|
||||||
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]
|
||||||
|
rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f w) Complex.I 1]
|
||||||
|
conv =>
|
||||||
|
right
|
||||||
|
right
|
||||||
|
intro w
|
||||||
|
rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)]
|
||||||
|
|
||||||
|
|
||||||
theorem MeasureTheory.integral2_divergence₃
|
theorem MeasureTheory.integral2_divergence₃
|
||||||
|
|
@ -106,9 +203,9 @@ theorem integral_divergence₅
|
||||||
exact h₁f
|
exact h₁f
|
||||||
|
|
||||||
let A := integral_divergence₄ (-Complex.I • F) F h₁g h₁f lowerLeft.re upperRight.im upperRight.re lowerLeft.im
|
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 ℝ _ F z := by rfl
|
have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv _ F z := by rfl
|
||||||
conv at A in (fderiv ℝ F _) _ => rw [this]
|
conv at A in (fderiv ℝ F _) _ => rw [this]
|
||||||
have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv ℝ _ (-Complex.I • F) z := by rfl
|
have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv _ (-Complex.I • F) z := by rfl
|
||||||
conv at A in (fderiv ℝ (-Complex.I • F) _) _ => rw [this]
|
conv at A in (fderiv ℝ (-Complex.I • F) _) _ => rw [this]
|
||||||
conv at A =>
|
conv at A =>
|
||||||
left
|
left
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue