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

18
Nevanlinna/complexHarmonic.lean
View File

@ -128,13 +128,20 @@ theorem logabs_of_holomorphic_is_harmonic
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
simp simp
conv =>
arg 3
intro x
rw [← Complex.reCLM_apply, ← Complex.imCLM_apply]
apply ContDiff.add apply ContDiff.add
apply ContDiff.mul apply ContDiff.mul
sorry apply ContinuousLinearMap.contDiff Complex.reCLM
apply ContinuousLinearMap.contDiff Complex.reCLM
apply ContDiff.mul
apply ContinuousLinearMap.contDiff Complex.imCLM
apply ContinuousLinearMap.contDiff Complex.imCLM
constructor constructor
· -- logabs f is real C² · -- 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‖) = (Real.log ∘ Complex.normSq ∘ f) / 2 := by
funext z funext z
simp simp
@ -143,8 +150,10 @@ theorem logabs_of_holomorphic_is_harmonic
rw [Real.log_sqrt] rw [Real.log_sqrt]
exact Complex.normSq_nonneg (f z) exact Complex.normSq_nonneg (f z)
rw [this] rw [this]
have : Real.log ∘ ⇑Complex.normSq ∘ f / 2 = (fun z ↦ (1 / 2) • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by have : Real.log ∘ ⇑Complex.normSq ∘ f / 2 = (fun z ↦ (1 / (2 : ℝ)) • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
sorry funext z
simp
exact div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2
rw [this] rw [this]
apply contDiff_iff_contDiffAt.2 apply contDiff_iff_contDiffAt.2
@ -160,4 +169,5 @@ theorem logabs_of_holomorphic_is_harmonic
exact ContDiff.contDiffAt f_is_real_C2 exact ContDiff.contDiffAt f_is_real_C2
· -- Laplace vanishes · -- Laplace vanishes
sorry sorry