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

Cleanup

This commit is contained in:
Stefan Kebekus 2024-05-06 09:01:43 +02:00
parent a55b084031
commit c44f4fe3b0
2 changed files with 6 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Nevanlinna/cauchyRiemann.lean
View File

@ -3,6 +3,7 @@ import Mathlib.Analysis.Complex.RealDeriv
variable {z : ℂ} {f : ℂ → ℂ} 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
@ -10,6 +11,7 @@ theorem CauchyRiemann₁ : (DifferentiableAt ℂ f z)
nth_rewrite 1 [← mul_one Complex.I] nth_rewrite 1 [← mul_one Complex.I]
exact ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f z) Complex.I 1 exact ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f z) Complex.I 1
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
@ -17,6 +19,7 @@ theorem CauchyRiemann₂ : (DifferentiableAt ℂ f z)
rw [DifferentiableAt.lineDeriv_eq_fderiv (h.restrictScalars ℝ)] rw [DifferentiableAt.lineDeriv_eq_fderiv (h.restrictScalars ℝ)]
exact CauchyRiemann₁ h exact CauchyRiemann₁ h
theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z) theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
→ (lineDeriv ℝ (Complex.reCLM ∘ f) z 1 = lineDeriv ℝ (Complex.imCLM ∘ f) z Complex.I) → (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) ∧ (lineDeriv ℝ (Complex.reCLM ∘ f) z Complex.I = -lineDeriv ℝ (Complex.imCLM ∘ f) z 1)

6
Nevanlinna/complexHarmonic.lean
View File

@ -20,7 +20,6 @@ noncomputable def Complex.laplace : (ℂ → ℂ) → (ℂ → ℂ) := by
def Harmonic (f : ℂ → ℂ) : Prop := def Harmonic (f : ℂ → ℂ) : Prop :=
(ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0) (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
#check second_derivative_symmetric
lemma zwoDiff (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) : ∀ z a b : ℝ × ℝ, 0 = 1 := by lemma zwoDiff (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) : ∀ z a b : ℝ × ℝ, 0 = 1 := by
intro z a b intro z a b
@ -61,13 +60,14 @@ lemma derivSymm (f : ℂ → ℂ) (h : Differentiable ℝ f) :
dsimp [f'', f'] at A dsimp [f'', f'] at A
apply A apply A
theorem re_comp_holomorphic_is_harmonic (f : ℂ → ℂ) :
theorem holomorphic_is_harmonic (f : ℂ → ℂ) :
Differentiable ℂ f → Harmonic f := by Differentiable ℂ f → Harmonic f := by
intro h intro h
constructor constructor
· -- Complex.reCLM ∘ f is two times real continuously differentiable · -- f is two times real continuously differentiable
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h) exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
· -- Laplace of f is zero · -- Laplace of f is zero