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-30 10:49:16 +02:00
parent 7f10e28525
commit ac3cd65bf2
1 changed files with 6 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
Nevanlinna/complexHarmonic.lean
View File

@ -220,16 +220,16 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
-- Suffices to show Harmonic (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f) -- Suffices to show Harmonic (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f)
-- THIS IS WHERE WE USE h₃ -- THIS IS WHERE WE USE h₃
have : Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f := by have : ∀ z ∈ s, (Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f)) z = (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f) z := by
intro z hz
unfold Function.comp unfold Function.comp
funext z
simp simp
rw [Complex.log_mul_eq_add_log_iff] rw [Complex.log_mul_eq_add_log_iff]
have : Complex.arg ((starRingEnd ℂ) (f z)) = - Complex.arg (f z) := by have : Complex.arg ((starRingEnd ℂ) (f z)) = - Complex.arg (f z) := by
rw [Complex.arg_conj] rw [Complex.arg_conj]
have : ¬ Complex.arg (f z) = Real.pi := by have : ¬ Complex.arg (f z) = Real.pi := by
exact Complex.slitPlane_arg_ne_pi (h₃ z) exact Complex.slitPlane_arg_ne_pi (h₃ z hz)
simp simp
tauto tauto
rw [this] rw [this]
@ -237,8 +237,9 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
constructor constructor
· exact Real.pi_pos · exact Real.pi_pos
· exact Real.pi_nonneg · exact Real.pi_nonneg
exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z) exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz)
exact h₂ z exact h₂ z hz
rw [this] rw [this]
apply harmonic_add_harmonic_is_harmonic apply harmonic_add_harmonic_is_harmonic