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-08 07:15:34 +02:00
parent 6061fa4279
commit 631b1bad70
1 changed files with 11 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
Nevanlinna/complexHarmonic.lean
View File

@ -39,7 +39,17 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
· -- Laplace of f is zero · -- Laplace of f is zero
unfold Complex.laplace unfold Complex.laplace
rw [CauchyRiemann₄ h] rw [CauchyRiemann₄ h]
rw [partialDeriv_smul₂ fI_is_real_differentiable]
let l : ℂ →L[ℝ] ℂ := by
--
sorry --(fun x ↦ Complex.I • x)
have : (Complex.I • Real.partialDeriv 1 f) = (l ∘ (Real.partialDeriv 1 f)) := by
sorry
rw [this]
rw [partialDeriv_compContLin]
--rw [partialDeriv_smul₂ fI_is_real_differentiable]
rw [partialDeriv_comm f_is_real_C2 Complex.I 1] rw [partialDeriv_comm f_is_real_C2 Complex.I 1]
rw [CauchyRiemann₄ h] rw [CauchyRiemann₄ h]
rw [partialDeriv_smul₂ fI_is_real_differentiable] rw [partialDeriv_smul₂ fI_is_real_differentiable]