nevanlinna/Nevanlinna/cauchyRiemann.lean

85 lines
2.4 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import Mathlib.Analysis.Calculus.LineDeriv.Basic
import Mathlib.Analysis.Complex.RealDeriv
import Nevanlinna.partialDeriv
variable {z : } {f : }
theorem CauchyRiemann₁ : (DifferentiableAt f z)
→ (fderiv f z) Complex.I = Complex.I * (fderiv f z) 1 := by
intro h
rw [DifferentiableAt.fderiv_restrictScalars h]
nth_rewrite 1 [← mul_one Complex.I]
exact ContinuousLinearMap.map_smul_of_tower (fderiv f z) Complex.I 1
theorem CauchyRiemann₂ : (DifferentiableAt f z)
→ lineDeriv f z Complex.I = Complex.I * lineDeriv f z 1 := by
intro h
rw [DifferentiableAt.lineDeriv_eq_fderiv (h.restrictScalars )]
rw [DifferentiableAt.lineDeriv_eq_fderiv (h.restrictScalars )]
exact CauchyRiemann₁ h
theorem CauchyRiemann₃ : (DifferentiableAt f z)
→ (lineDeriv (Complex.reCLM ∘ f) z 1 = lineDeriv (Complex.imCLM ∘ f) z Complex.I)
∧ (lineDeriv (Complex.reCLM ∘ f) z Complex.I = -lineDeriv (Complex.imCLM ∘ f) z 1)
:= by
intro h
have ContinuousLinearMap.comp_lineDeriv : ∀ w : , ∀ l : →L[] , lineDeriv (l ∘ f) z w = l ((fderiv f z) w) := by
intro w l
rw [DifferentiableAt.lineDeriv_eq_fderiv]
rw [fderiv.comp]
simp
fun_prop
exact h.restrictScalars
apply (ContinuousLinearMap.differentiableAt l).comp
exact h.restrictScalars
repeat
rw [ContinuousLinearMap.comp_lineDeriv]
rw [CauchyRiemann₁ h, Complex.I_mul]
simp
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 CauchyRiemann₅ {F : Type*} [NormedAddCommGroup F] [NormedSpace F] {f : → F} {z : } : (DifferentiableAt f z)
→ partialDeriv Complex.I f z = Complex.I • partialDeriv 1 f z := by
intro h
unfold partialDeriv
conv =>
left
rw [DifferentiableAt.fderiv_restrictScalars h]
simp
rw [← mul_one Complex.I]
rw [← smul_eq_mul]
conv =>
right
right
rw [DifferentiableAt.fderiv_restrictScalars h]
simp