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-30 10:41:10 +02:00
parent 2544242b13
commit 7f10e28525
1 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
Nevanlinna/complexHarmonic.lean
View File

@ -89,7 +89,7 @@ theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G}
exact ContDiff.restrict_scalars ℝ h.1 exact ContDiff.restrict_scalars ℝ h.1
theorem harmonicOn_comp_CLM_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l : F₁ →L[ℝ] G} (h : HarmonicOn f s) : theorem harmonicOn_comp_CLM_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l : F₁ →L[ℝ] G} (hs : IsOpen s) (h : HarmonicOn f s) :
HarmonicOn (l ∘ f) s := by HarmonicOn (l ∘ f) s := by
constructor constructor
@ -97,15 +97,14 @@ theorem harmonicOn_comp_CLM_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l :
apply ContDiffOn.continuousLinearMap_comp apply ContDiffOn.continuousLinearMap_comp
exact h.1 exact h.1
· -- Vanishing of Laplace · -- Vanishing of Laplace
rw [laplace_compContLin]
simp
intro z zHyp intro z zHyp
rw [laplace_compContLinAt]
simp
rw [h.2 z] rw [h.2 z]
simp simp
assumption assumption
apply ContDiffOn.contDiffAt h.1
exact IsOpen.mem_nhds hs zHyp
theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ] G₁} : theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ] G₁} :
@ -200,15 +199,16 @@ theorem antiholomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f)
theorem log_normSq_of_holomorphicOn_is_harmonicOn theorem log_normSq_of_holomorphicOn_is_harmonicOn
{f : ℂ → ℂ} {f : ℂ → ℂ}
{s : Set ℂ} {s : Set ℂ}
(hs : IsOpen s)
(h₁ : DifferentiableOn ℂ f s) (h₁ : DifferentiableOn ℂ f s)
(h₂ : ∀ z ∈ s, f z ≠ 0) (h₂ : ∀ z ∈ s, f z ≠ 0)
(h₃ : ∀ z ∈ s, f z ∈ Complex.slitPlane) : (h₃ : ∀ z ∈ s, f z ∈ Complex.slitPlane) :
HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by
suffices hyp : Harmonic (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) from suffices hyp : HarmonicOn (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) s from
(harmonic_comp_CLM_is_harmonic hyp : Harmonic (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f)) (harmonicOn_comp_CLM_is_harmonicOn hs hyp : HarmonicOn (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) s)
suffices hyp : Harmonic (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) from by suffices hyp : HarmonicOn (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) s from by
have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f) := by have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f) := by
funext z funext z
simp simp