Update complexHarmonic.lean
This commit is contained in:
Stefan Kebekus
parent
bcb639a5be
commit
82fdc5ac37
|
|
@ -26,6 +26,17 @@ def Harmonic (f : ℂ → F) : Prop :=
|
||||||
(ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
|
(ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
|
||||||
|
|
||||||
|
|
||||||
|
theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F₁} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) :
|
||||||
|
Harmonic (f₁ + f₂) := by
|
||||||
|
constructor
|
||||||
|
· exact ContDiff.add h₁.1 h₂.1
|
||||||
|
· rw [laplace_add h₁.1 h₂.1]
|
||||||
|
simp
|
||||||
|
intro z
|
||||||
|
rw [h₁.2 z, h₂.2 z]
|
||||||
|
simp
|
||||||
|
|
||||||
|
|
||||||
theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G} (h : Harmonic f) :
|
theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G} (h : Harmonic f) :
|
||||||
Harmonic (l ∘ f) := by
|
Harmonic (l ∘ f) := by
|
||||||
|
|
||||||
|
|
@ -138,151 +149,72 @@ theorem log_normSq_of_holomorphic_is_harmonic
|
||||||
(h₃ : ∀ z, f z ∈ Complex.slitPlane) :
|
(h₃ : ∀ z, f z ∈ Complex.slitPlane) :
|
||||||
Harmonic (Real.log ∘ Complex.normSq ∘ f) := by
|
Harmonic (Real.log ∘ Complex.normSq ∘ f) := by
|
||||||
|
|
||||||
|
-- Suffices to show Harmonic (⇑Complex.ofRealCLM ∘ Real.log ∘ ⇑Complex.normSq ∘ f)
|
||||||
|
let F := Real.log ∘ Complex.normSq ∘ f
|
||||||
|
have : Harmonic (Complex.ofRealCLM ∘ F) → Harmonic F := by
|
||||||
|
intro hyp
|
||||||
|
have t₁ : Harmonic (Complex.reCLM ∘ Complex.ofRealCLM ∘ F) := harmonic_comp_CLM_is_harmonic hyp
|
||||||
|
have t₂ : Complex.reCLM ∘ Complex.ofRealCLM ∘ F = F := rfl
|
||||||
|
rw [t₂] at t₁
|
||||||
|
exact t₁
|
||||||
|
apply this
|
||||||
|
dsimp [F]
|
||||||
|
|
||||||
|
-- Suffices to show Harmonic (Complex.log ∘ Complex.ofRealCLM ∘ Complex.normSq ∘ f)
|
||||||
|
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]
|
||||||
|
|
||||||
/- We start with a number of lemmas on regularity of all the functions involved -/
|
-- Suffices to show Harmonic (Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f))
|
||||||
|
have : Complex.ofRealCLM ∘ ⇑Complex.normSq ∘ f = ((starRingEnd ℂ) ∘ f) * f := by
|
||||||
-- The norm square is real C²
|
funext z
|
||||||
have normSq_is_real_C2 : ContDiff ℝ 2 Complex.normSq := by
|
|
||||||
unfold Complex.normSq
|
|
||||||
simp
|
simp
|
||||||
conv =>
|
exact Complex.normSq_eq_conj_mul_self
|
||||||
arg 3
|
rw [this]
|
||||||
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²
|
-- Suffices to show Harmonic (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f)
|
||||||
have log_f_is_holomorphic : Differentiable ℂ (Complex.log ∘ f) := by
|
-- THIS IS WHERE WE USE h₃
|
||||||
intro z
|
have : Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f := by
|
||||||
apply DifferentiableAt.comp
|
unfold Function.comp
|
||||||
exact Complex.differentiableAt_log (h₃ z)
|
funext 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
|
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
|
exact h₂ z
|
||||||
apply ContDiff.comp_contDiffAt z normSq_is_real_C2
|
rw [this]
|
||||||
exact ContDiff.contDiffAt f_is_real_C2
|
|
||||||
|
|
||||||
have t₂ : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
|
apply harmonic_add_harmonic_is_harmonic
|
||||||
|
have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
|
||||||
funext z
|
funext z
|
||||||
unfold Function.comp
|
unfold Function.comp
|
||||||
rw [Complex.log_conj]
|
rw [Complex.log_conj]
|
||||||
rfl
|
rfl
|
||||||
exact Complex.slitPlane_arg_ne_pi (h₃ z)
|
exact Complex.slitPlane_arg_ne_pi (h₃ z)
|
||||||
|
rw [this]
|
||||||
|
rw [← harmonic_iff_comp_CLE_is_harmonic]
|
||||||
|
|
||||||
constructor
|
repeat
|
||||||
· -- logabs f is real C²
|
apply holomorphic_is_harmonic
|
||||||
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]
|
|
||||||
|
|
||||||
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
|
|
||||||
|
|
||||||
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
|
||||||
simp
|
apply DifferentiableAt.comp
|
||||||
rw [(holomorphic_is_harmonic log_f_is_holomorphic).2 z]
|
exact Complex.differentiableAt_log (h₃ z)
|
||||||
simp
|
exact h₁ z
|
||||||
|
|
||||||
-- 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
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue