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 08:54:28 +02:00
parent 90d3aceb95
commit a5bf92552c
1 changed files with 18 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
nevanlinna/cauchyRiemann.lean
View File

@ -11,40 +11,25 @@ import Mathlib.Analysis.Calculus.Conformal.NormedSpace
import Mathlib.Analysis.Calculus.FDeriv.Basic import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
variable {z : ℂ} {f : ℂ → ℂ} variable {z : ℂ} {f : ℂ → ℂ} {h : DifferentiableAt ℂ f z}
example (h : DifferentiableAt ℂ f z) : f z = 0 := by
theorem CauchyRiemann₁ : fderiv ℝ f z Complex.I = Complex.I * fderiv ℝ f z 1 := by
let A := fderiv ℂ f z let A := fderiv ℂ f z
let B := fderiv ℝ f have t₁ : A (Complex.I • 1) = Complex.I • (A 1) := by
let C : HasFDerivAt f (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) z := h.hasFDerivAt.restrictScalars ℝ
let D := ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)
let E := D 1
let F := D Complex.I
have : A (Complex.I • 1) = Complex.I • (A 1) := by
exact ContinuousLinearMap.map_smul_of_tower A Complex.I 1 exact ContinuousLinearMap.map_smul_of_tower A Complex.I 1
let AR := (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) let AR := (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))
have : AR (Complex.I • 1) = Complex.I • (AR 1) := by have t₂ : AR (Complex.I • 1) = Complex.I • (AR 1) := by
exact this exact t₁
have t₂a : Complex.I * (AR 1) = Complex.I • (AR 1) := by
let f₂ := fun x ↦ lineDeriv ℝ f x ⟨0,1⟩ exact rfl
have : lineDeriv ℝ f z Complex.I = (fderiv ℝ f z) Complex.I := by rw [← t₂a] at t₂
apply DifferentiableAt.lineDeriv_eq_fderiv have t₂b : Complex.I • 1 = Complex.I := by
apply h.restrictScalars ℝ simp
have t₂c : AR Complex.I = Complex.I • (AR 1) := by
have : D Complex.I = Complex.I * (D 1) := by simp at t₂
-- x exact t₂
let C : HasFDerivAt f (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) z := h.hasFDerivAt.restrictScalars ℝ
sorry have t₃ : fderiv ℝ f z = ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z) := by
exact DifferentiableAt.fderiv_restrictScalars ℝ h
have : HasFDerivAt f A z := by rw [t₃]
exact DifferentiableAt.hasFDerivAt h exact t₂c
have : HasFDerivAt f (B z) z := by
sorry
sorry