kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update cauchyRiemann.lean

This commit is contained in:
Stefan Kebekus 2024-04-29 19:48:37 +02:00
parent 38eaf677f9
commit 2d2a21be72
1 changed files with 5 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

43
nevanlinna/cauchyRiemann.lean
View File

@ -1,15 +1,4 @@
--import Mathlib.Analysis.Calculus.Conformal.NormedSpace
--import Mathlib.Analysis.Calculus.ContDiff.Basic
--import Mathlib.Analysis.Calculus.ContDiff.Defs
--import Mathlib.Analysis.Calculus.Deriv.Linear
--import Mathlib.Analysis.Calculus.FDeriv.Basic
--import Mathlib.Analysis.Calculus.FDeriv.Comp
--import Mathlib.Analysis.Calculus.FDeriv.Linear
--import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
import Mathlib.Analysis.Calculus.LineDeriv.Basic import Mathlib.Analysis.Calculus.LineDeriv.Basic
--import Mathlib.Analysis.Complex.Basic
--import Mathlib.Analysis.Complex.CauchyIntegral
--import Mathlib.Analysis.Complex.Conformal
import Mathlib.Analysis.Complex.RealDeriv import Mathlib.Analysis.Complex.RealDeriv
variable {z : ℂ} {f : ℂ → ℂ} variable {z : ℂ} {f : ℂ → ℂ}
@ -17,37 +6,15 @@ variable {z : ℂ} {f : ℂ → ℂ}
theorem CauchyRiemann₁ : (DifferentiableAt ℂ f z) theorem CauchyRiemann₁ : (DifferentiableAt ℂ f z)
→ (fderiv ℝ f z) Complex.I = Complex.I * (fderiv ℝ f z) 1 := by → (fderiv ℝ f z) Complex.I = Complex.I * (fderiv ℝ f z) 1 := by
intro h intro h
let A := fderiv ℂ f z rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
have t₁ : A (Complex.I • 1) = Complex.I • (A 1) := by nth_rewrite 1 [← mul_one Complex.I]
exact ContinuousLinearMap.map_smul_of_tower A Complex.I 1 exact ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f z) Complex.I 1
let AR := (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))
have t₂ : AR (Complex.I • 1) = Complex.I • (AR 1) := by
exact t₁
have t₂a : Complex.I * (AR 1) = Complex.I • (AR 1) := by
exact rfl
rw [← t₂a] at t₂
have t₂c : AR Complex.I = Complex.I • (AR 1) := by
simp at t₂
exact t₂
have t₃ : fderiv ℝ f z = ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z) := by
exact DifferentiableAt.fderiv_restrictScalars ℝ h
rw [t₃]
exact t₂c
theorem CauchyRiemann₂ : (DifferentiableAt ℂ f z) theorem CauchyRiemann₂ : (DifferentiableAt ℂ f z)
→ lineDeriv ℝ f z Complex.I = Complex.I * lineDeriv ℝ f z 1 := by → lineDeriv ℝ f z Complex.I = Complex.I * lineDeriv ℝ f z 1 := by
intro h intro h
rw [DifferentiableAt.lineDeriv_eq_fderiv (h.restrictScalars ℝ)]
have : lineDeriv ℝ f z Complex.I = (fderiv ℝ f z) Complex.I := by rw [DifferentiableAt.lineDeriv_eq_fderiv (h.restrictScalars ℝ)]
apply DifferentiableAt.lineDeriv_eq_fderiv
apply h.restrictScalars ℝ
rw [this]
have : lineDeriv ℝ f z 1 = (fderiv ℝ f z) 1 := by
apply DifferentiableAt.lineDeriv_eq_fderiv
apply h.restrictScalars ℝ
rw [this]
exact CauchyRiemann₁ h exact CauchyRiemann₁ h
theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z) theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)