Update complexHarmonic.lean

This commit is contained in:
Stefan Kebekus 2024-05-18 12:13:30 +02:00
parent 348492cc94
commit 7319bf60c0
1 changed files with 94 additions and 0 deletions

View File

@ -26,6 +26,23 @@ def Harmonic (f : → F) : Prop :=
(ContDiff 2 f) ∧ (∀ z, Complex.laplace f z = 0) (ContDiff 2 f) ∧ (∀ z, Complex.laplace f z = 0)
def HarmonicOn (f : → F) (s : Set ) : Prop :=
(ContDiffOn 2 f s) ∧ (∀ z ∈ s, Complex.laplace f z = 0)
theorem HarmonicOn_of_locally_HarmonicOn {f : → F} {s : Set } (h : ∀ x ∈ s, ∃ (u : Set ), IsOpen u ∧ x ∈ u ∧ HarmonicOn f (s ∩ u)) :
HarmonicOn f s := by
constructor
· apply contDiffOn_of_locally_contDiffOn
intro x xHyp
obtain ⟨u, uHyp⟩ := h x xHyp
use u
exact ⟨ uHyp.1, ⟨uHyp.2.1, uHyp.2.2.1⟩⟩
· intro x xHyp
obtain ⟨u, uHyp⟩ := h x xHyp
exact (uHyp.2.2.2) x ⟨xHyp, uHyp.2.1⟩
theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : → F} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) : theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : → F} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) :
Harmonic (f₁ + f₂) := by Harmonic (f₁ + f₂) := by
constructor constructor
@ -72,6 +89,21 @@ 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) :
HarmonicOn (l ∘ f) s := by
constructor
· -- Continuous differentiability
apply ContDiffOn.continuousLinearMap_comp
exact h.1
· rw [laplace_compContLin]
simp
intro z zHyp
rw [h.2 z]
simp
assumption
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₁} :
Harmonic f ↔ Harmonic (l ∘ f) := by Harmonic f ↔ Harmonic (l ∘ f) := by
@ -161,6 +193,68 @@ theorem antiholomorphic_is_harmonic {f : } (h : Differentiable f)
exact holomorphic_is_harmonic h exact holomorphic_is_harmonic h
theorem log_normSq_of_holomorphicOn_is_harmonicOn
{f : }
{s : Set }
(h₁ : DifferentiableOn f s)
(h₂ : ∀ z ∈ s, f z ≠ 0)
(h₃ : ∀ z ∈ s, f z ∈ Complex.slitPlane) :
HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by
suffices hyp : Harmonic (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) from
(harmonic_comp_CLM_is_harmonic hyp : Harmonic (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f))
suffices hyp : Harmonic (Complex.log ∘ (((starRingEnd ) ∘ f) * f)) from by
have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ (((starRingEnd ) ∘ f) * f) := by
funext z
simp
rw [Complex.ofReal_log (Complex.normSq_nonneg (f z))]
rw [Complex.normSq_eq_conj_mul_self]
rw [this]
exact hyp
-- Suffices to show Harmonic (Complex.log ∘ ⇑(starRingEnd ) ∘ f + Complex.log ∘ f)
-- THIS IS WHERE WE USE h₃
have : Complex.log ∘ (⇑(starRingEnd ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ) ∘ f + Complex.log ∘ f := by
unfold Function.comp
funext z
simp
rw [Complex.log_mul_eq_add_log_iff]
have : Complex.arg ((starRingEnd ) (f z)) = - Complex.arg (f z) := by
rw [Complex.arg_conj]
have : ¬ Complex.arg (f z) = Real.pi := by
exact Complex.slitPlane_arg_ne_pi (h₃ z)
simp
tauto
rw [this]
simp
constructor
· exact Real.pi_pos
· exact Real.pi_nonneg
exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
exact h₂ z
rw [this]
apply harmonic_add_harmonic_is_harmonic
have : Complex.log ∘ ⇑(starRingEnd ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
funext z
unfold Function.comp
rw [Complex.log_conj]
rfl
exact Complex.slitPlane_arg_ne_pi (h₃ z)
rw [this]
rw [← harmonic_iff_comp_CLE_is_harmonic]
repeat
apply holomorphic_is_harmonic
intro z
apply DifferentiableAt.comp
exact Complex.differentiableAt_log (h₃ z)
exact h₁ z
theorem log_normSq_of_holomorphic_is_harmonic theorem log_normSq_of_holomorphic_is_harmonic
{f : } {f : }
(h₁ : Differentiable f) (h₁ : Differentiable f)