Update complexHarmonic.lean

This commit is contained in:
Stefan Kebekus 2024-05-15 10:09:22 +02:00
parent a60e07e602
commit 058ea29a64
1 changed files with 61 additions and 2 deletions

View File

@ -117,13 +117,17 @@ theorem im_of_holomorphic_is_harmonic {f : } (h : Differentiable
theorem logabs_of_holomorphic_is_harmonic theorem logabs_of_holomorphic_is_harmonic
{f : } {f : }
(h₁ : Differentiable f) (h₁ : Differentiable f)
(h₂ : ∀ z, f z ≠ 0) : (h₂ : ∀ z, f z ≠ 0)
(h₃ : ∀ z, f z ∈ Complex.slitPlane) :
Harmonic (fun z ↦ Real.log ‖f z‖) := by Harmonic (fun z ↦ Real.log ‖f z‖) := by
-- f is real C² -- f is real C²
have f_is_real_C2 : ContDiff 2 f := have f_is_real_C2 : ContDiff 2 f :=
ContDiff.restrict_scalars (Differentiable.contDiff h₁) ContDiff.restrict_scalars (Differentiable.contDiff h₁)
-- The norm square is z * z.conj
have normSq_conj : ∀ (z : ), (starRingEnd ) z * z = ↑‖z‖ ^ 2 := Complex.conj_mul'
-- The norm square is real C² -- The norm square is real C²
have normSq_is_real_C2 : ContDiff 2 Complex.normSq := by have normSq_is_real_C2 : ContDiff 2 Complex.normSq := by
unfold Complex.normSq unfold Complex.normSq
@ -169,5 +173,60 @@ theorem logabs_of_holomorphic_is_harmonic
exact ContDiff.contDiffAt f_is_real_C2 exact ContDiff.contDiffAt f_is_real_C2
· -- Laplace vanishes · -- 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
sorry
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]
sorry sorry
sorry