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-14 17:24:34 +02:00
parent 06f8de2f56
commit a60e07e602
1 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
Nevanlinna/complexHarmonic.lean
View File

@ -142,18 +142,18 @@ theorem logabs_of_holomorphic_is_harmonic
constructor
· -- logabs f is real C²
have : (fun z ↦ Real.log ‖f z‖) = (Real.log ∘ Complex.normSq ∘ f) / 2 := by
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]
exact Complex.normSq_nonneg (f z)
rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
exact Complex.normSq_nonneg (f z)
rw [this]
have : Real.log ∘ ⇑Complex.normSq ∘ f / 2 = (fun z ↦ (1 / (2 : ℝ)) • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
funext z
have : (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : ℝ)⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
simp
exact div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2
rw [this]
apply contDiff_iff_contDiffAt.2
@ -169,5 +169,5 @@ theorem logabs_of_holomorphic_is_harmonic
exact ContDiff.contDiffAt f_is_real_C2
· -- Laplace vanishes
sorry