Update complexHarmonic.lean

This commit is contained in:
Stefan Kebekus 2024-05-16 21:46:01 +02:00
parent 077bace964
commit 71ad6aa67e
1 changed files with 190 additions and 22 deletions

View File

@ -17,13 +17,47 @@ import Nevanlinna.laplace
import Nevanlinna.partialDeriv import Nevanlinna.partialDeriv
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace F] variable {F : Type*} [NormedAddCommGroup F] [NormedSpace F]
variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace F₁] [CompleteSpace F₁]
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace G]
variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace G₁] [CompleteSpace G₁]
def Harmonic (f : → F) : Prop := def Harmonic (f : → F) : Prop :=
(ContDiff 2 f) ∧ (∀ z, Complex.laplace f z = 0) (ContDiff 2 f) ∧ (∀ z, Complex.laplace f z = 0)
theorem holomorphic_is_harmonic {f : } (h : Differentiable f) : theorem harmonic_comp_CLM_is_harmonic {f : → F₁} {l : F₁ →L[] G} (h : Harmonic f) :
Harmonic (l ∘ f) := by
constructor
· -- Continuous differentiability
apply ContDiff.comp
exact ContinuousLinearMap.contDiff l
exact ContDiff.restrict_scalars (Differentiable.contDiff h)
· rw [laplace_compContLin]
simp
intro z
rw [h.2 z]
simp
exact ContDiff.restrict_scalars (Differentiable.contDiff h)
theorem harmonic_iff_comp_CLE_is_harmonic {f : → F₁} {l : F₁ ≃L[] G₁} :
Harmonic f ↔ Harmonic (l ∘ f) := by
constructor
· have : l ∘ f = (l : F₁ →L[] G₁) ∘ f := by rfl
rw [this]
exact harmonic_comp_CLM_is_harmonic
· have : f = (l.symm : G₁ →L[] F₁) ∘ l ∘ f := by
funext z
unfold Function.comp
simp
nth_rewrite 2 [this]
exact harmonic_comp_CLM_is_harmonic
theorem holomorphic_is_harmonic {f : → F₁} (h : Differentiable f) :
Harmonic f := by Harmonic f := by
-- f is real C² -- f is real C²
@ -83,36 +117,170 @@ theorem holomorphic_is_harmonic {f : } (h : Differentiable f) :
exact fI_is_real_differentiable exact fI_is_real_differentiable
theorem re_of_holomorphic_is_harmonic {f : } (h : Differentiable f) : theorem re_of_holomorphic_is_harmonic {f : } (h : Differentiable f) :
Harmonic (Complex.reCLM ∘ f) := by Harmonic (Complex.reCLM ∘ f) := by
apply harmonic_comp_CLM_is_harmonic
constructor exact holomorphic_is_harmonic h
· -- Continuous differentiability
apply ContDiff.comp
exact ContinuousLinearMap.contDiff Complex.reCLM
exact ContDiff.restrict_scalars (Differentiable.contDiff h)
· rw [laplace_compContLin]
simp
intro z
rw [(holomorphic_is_harmonic h).right z]
simp
exact ContDiff.restrict_scalars (Differentiable.contDiff h)
theorem im_of_holomorphic_is_harmonic {f : } (h : Differentiable f) : theorem im_of_holomorphic_is_harmonic {f : } (h : Differentiable f) :
Harmonic (Complex.imCLM ∘ f) := by Harmonic (Complex.imCLM ∘ f) := by
apply harmonic_comp_CLM_is_harmonic
exact holomorphic_is_harmonic h
theorem log_normSq_of_holomorphic_is_harmonic
{f : }
(h₁ : Differentiable f)
(h₂ : ∀ z, f z ≠ 0)
(h₃ : ∀ z, f z ∈ Complex.slitPlane) :
Harmonic (Real.log ∘ Complex.normSq ∘ f) := by
/- We start with a number of lemmas on regularity of all the functions involved -/
-- The norm square is real C²
have normSq_is_real_C2 : ContDiff 2 Complex.normSq := by
unfold Complex.normSq
simp
conv =>
arg 3
intro x
rw [← Complex.reCLM_apply, ← Complex.imCLM_apply]
apply ContDiff.add
apply ContDiff.mul
apply ContinuousLinearMap.contDiff Complex.reCLM
apply ContinuousLinearMap.contDiff Complex.reCLM
apply ContDiff.mul
apply ContinuousLinearMap.contDiff Complex.imCLM
apply ContinuousLinearMap.contDiff Complex.imCLM
-- f is real C²
have f_is_real_C2 : ContDiff 2 f :=
ContDiff.restrict_scalars (Differentiable.contDiff h₁)
-- Complex.log ∘ f is real C²
have log_f_is_holomorphic : Differentiable (Complex.log ∘ f) := by
intro z
apply DifferentiableAt.comp
exact Complex.differentiableAt_log (h₃ z)
exact h₁ z
-- Real.log |f|² is real C²
have t₄ : ContDiff 2 (Real.log ∘ ⇑Complex.normSq ∘ f) := by
rw [contDiff_iff_contDiffAt]
intro z
apply ContDiffAt.comp
apply Real.contDiffAt_log.mpr
simp
exact h₂ z
apply ContDiff.comp_contDiffAt z normSq_is_real_C2
exact ContDiff.contDiffAt f_is_real_C2
have t₂ : 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)
constructor constructor
· -- Continuous differentiability · -- logabs f is real C²
apply ContDiff.comp have : (fun z ↦ Real.log ‖f z‖) = (2 : )⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
exact ContinuousLinearMap.contDiff Complex.imCLM funext z
exact ContDiff.restrict_scalars (Differentiable.contDiff h) simp
· rw [laplace_compContLin] unfold Complex.abs
simp
rw [Real.log_sqrt]
rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
exact Complex.normSq_nonneg (f z)
rw [this]
have : (2 : )⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : )⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
exact rfl
rw [this]
apply ContDiff.const_smul
exact t₄
· -- Laplace vanishes
have : (fun z ↦ Real.log ‖f z‖) = (2 : )⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
funext z
simp
unfold Complex.abs
simp
rw [Real.log_sqrt]
rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
exact Complex.normSq_nonneg (f z)
rw [this]
rw [laplace_smul]
simp simp
have : ∀ (z : ), Complex.laplace (Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 ↔ Complex.laplace (Complex.ofRealCLM ∘ Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 := by
intro z
rw [laplace_compContLin]
simp
-- ContDiff 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
exact t₄
conv =>
intro z
rw [this z]
have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ Complex.ofRealCLM ∘ Complex.normSq ∘ f := by
unfold Function.comp
funext z
apply Complex.ofReal_log
exact Complex.normSq_nonneg (f z)
rw [this]
have : Complex.ofRealCLM ∘ ⇑Complex.normSq ∘ f = ((starRingEnd ) ∘ f) * f := by
funext z
simp
exact Complex.normSq_eq_conj_mul_self
rw [this]
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]
rw [laplace_add]
rw [t₂, laplace_compCLE]
intro z intro z
rw [(holomorphic_is_harmonic h).right z]
simp simp
exact ContDiff.restrict_scalars (Differentiable.contDiff h) rw [(holomorphic_is_harmonic log_f_is_holomorphic).2 z]
simp
-- ContDiff 2 (Complex.log ∘ f)
exact ContDiff.restrict_scalars (Differentiable.contDiff log_f_is_holomorphic)
-- ContDiff 2 (Complex.log ∘ ⇑(starRingEnd ) ∘ f)
rw [t₂]
apply ContDiff.comp
exact ContinuousLinearEquiv.contDiff Complex.conjCLE
exact ContDiff.restrict_scalars (Differentiable.contDiff log_f_is_holomorphic)
-- ContDiff 2 (Complex.log ∘ f)
exact ContDiff.restrict_scalars (Differentiable.contDiff log_f_is_holomorphic)
-- ContDiff 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
exact t₄
theorem logabs_of_holomorphic_is_harmonic theorem logabs_of_holomorphic_is_harmonic