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-15 21:17:42 +02:00
parent 1c34aee7be
commit bfeade4095
1 changed files with 9 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
Nevanlinna/complexHarmonic.lean
View File

@ -159,6 +159,7 @@ theorem logabs_of_holomorphic_is_harmonic
have : (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : ℝ)⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by have : (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : ℝ)⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
simp simp
exact rfl
rw [this] rw [this]
apply contDiff_iff_contDiffAt.2 apply contDiff_iff_contDiffAt.2
@ -236,11 +237,11 @@ theorem logabs_of_holomorphic_is_harmonic
exact Complex.differentiableAt_log (h₃ z) exact Complex.differentiableAt_log (h₃ z)
exact h₁ z exact h₁ z
have : Complex.laplace (Complex.log ∘ f) = 0 := by have t₁: Complex.laplace (Complex.log ∘ f) = 0 := by
let A := holomorphic_is_harmonic this let A := holomorphic_is_harmonic this
funext z funext z
exact A.2 z exact A.2 z
rw [this] rw [t₁]
simp simp
have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f := by have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f := by
@ -253,13 +254,9 @@ theorem logabs_of_holomorphic_is_harmonic
have : ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by have : ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
rfl rfl
rw [this] rw [this]
have : ContDiff ℝ 2 (Complex.log ∘ f) := by sorry rw [laplace_compCLE]
rw [t₁]
have : Complex.laplace (⇑Complex.conjCLE ∘ f) = ⇑Complex.conjCLE ∘ Complex.laplace (f) := by simp
sorry
sorry
sorry
sorry sorry
sorry sorry