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 08:32:06 +02:00
parent 5ce2b83c20
commit 69a35228ee
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
Nevanlinna/complexHarmonic.lean
View File

@ -46,9 +46,14 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
unfold Complex.laplace unfold Complex.laplace
rw [CauchyRiemann₄ h] rw [CauchyRiemann₄ h]
-- This lemma says that partial derivatives commute with complex scalar
-- multiplication. This is a consequence of partialDeriv_compContLin once we
-- note that complex scalar multiplication is continuous ℝ-linear.
have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → ℂ, Differentiable ℝ g → Real.partialDeriv v (s • g) = s • (Real.partialDeriv v g) := by have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → ℂ, Differentiable ℝ g → Real.partialDeriv v (s • g) = s • (Real.partialDeriv v g) := by
intro v s g hg intro v s g hg
-- Present scalar multiplication as a continuous ℝ-linear map. This is
-- horrible, there must be better ways to do that.
let sMuls : ℂ →L[ℝ] ℂ := let sMuls : ℂ →L[ℝ] ℂ :=
{ {
toFun := fun x ↦ s * x toFun := fun x ↦ s * x
@ -61,8 +66,11 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
ring ring
} }
-- Bring the goal into a form that is recognized by
-- partialDeriv_compContLin.
have : s • g = sMuls ∘ g := by rfl have : s • g = sMuls ∘ g := by rfl
rw [this] rw [this]
rw [partialDeriv_compContLin hg] rw [partialDeriv_compContLin hg]
rfl rfl