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

Update complexHarmonic.lean

This commit is contained in:
Stefan Kebekus 2024-05-06 17:01:10 +02:00
parent b03954eee9
commit 9ac79470cd
1 changed files with 22 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
Nevanlinna/complexHarmonic.lean
View File

@ -52,14 +52,25 @@ lemma l₂ {f : ℂ → ℂ} (hf : ContDiff ℝ 2 f) (z a b : ℂ) :
· simp · simp
theorem holomorphic_is_harmonic (f : ℂ → ℂ) : theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
Differentiable ℂ f → Harmonic f := by Harmonic f := by
-- f is real C²
have f_is_real_C2 : ContDiff ℝ 2 f :=
ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
-- f' is real C¹
have f'_is_real_C1 : ContDiff ℝ 1 (fderiv ℝ f) :=
(contDiff_succ_iff_fderiv.1 f_is_real_C2).right
-- f' is real differentiable
have f'_is_differentiable : Differentiable ℝ (fderiv ℝ f) :=
(contDiff_succ_iff_fderiv.1 f'_is_real_C1).left
intro h
constructor constructor
· -- f is two times real continuously differentiable · -- f is two times real continuously differentiable
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h) exact f_is_real_C2
· -- Laplace of f is zero · -- Laplace of f is zero
intro z intro z
@ -75,20 +86,14 @@ theorem holomorphic_is_harmonic (f : ℂ → ℂ) :
intro z intro z
rw [CauchyRiemann₁ (h z)] rw [CauchyRiemann₁ (h z)]
have t₂₀ : ContDiff ℝ 2 f := by exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
have t₀₀ : Differentiable ℝ (fun w => (fderiv ℝ f w)) := by have t₀ : ∀ z, DifferentiableAt ℝ (fun w ↦ (fderiv ℝ f w) 1) z := by
let A := (contDiff_succ_iff_fderiv.1 t₂₀).right
let B := (contDiff_succ_iff_fderiv.1 A).left
exact B
have t₀ : ∀ z, DifferentiableAt ℝ (fun w => (fderiv ℝ f w) 1) z := by
intro z intro z
let A := t₀₀ let A := f'_is_differentiable
fun_prop fun_prop
have t₁ : ∀ x, (fderiv ℝ (fun w => Complex.I * (fderiv ℝ f w) 1) z) x have t₁ : ∀ x, (fderiv ℝ (fun w ↦ Complex.I * (fderiv ℝ f w) 1) z) x
= Complex.I * ((fderiv ℝ (fun w => (fderiv ℝ f w) 1) z) x) := by = Complex.I * ((fderiv ℝ (fun w ↦ (fderiv ℝ f w) 1) z) x) := by
intro x intro x
rw [fderiv_const_mul] rw [fderiv_const_mul]
simp simp
@ -97,11 +102,11 @@ theorem holomorphic_is_harmonic (f : ℂ → ℂ) :
have t₂ : (fderiv ℝ (fun w => (fderiv ℝ f w) 1) z) Complex.I have t₂ : (fderiv ℝ (fun w => (fderiv ℝ f w) 1) z) Complex.I
= (fderiv ℝ (fun w => (fderiv ℝ f w) Complex.I) z) 1 := by = (fderiv ℝ (fun w => (fderiv ℝ f w) Complex.I) z) 1 := by
let A := derivSymm f t₂₀ z 1 Complex.I let A := derivSymm f f_is_real_C2 z 1 Complex.I
let B := l₂ t₂₀ z Complex.I 1 let B := l₂ f_is_real_C2 z Complex.I 1
rw [← B] rw [← B]
rw [A] rw [A]
let C := l₂ t₂₀ z 1 Complex.I let C := l₂ f_is_real_C2 z 1 Complex.I
rw [C] rw [C]
rw [t₂] rw [t₂]