kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update complexHarmonic.examples.lean

This commit is contained in:
Stefan Kebekus 2024-06-03 18:45:31 +02:00
parent 89793b75d8
commit c595da782c
1 changed files with 16 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
Nevanlinna/complexHarmonic.examples.lean
View File

@ -246,8 +246,7 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
{s : Set ℂ} {s : Set ℂ}
(hs : IsOpen s) (hs : IsOpen s)
(h₁ : DifferentiableOn ℂ f s) (h₁ : DifferentiableOn ℂ f s)
(h₂ : ∀ z ∈ s, f z ≠ 0) (h₂ : ∀ z ∈ s, f z ≠ 0) :
(h₃ : ∀ z ∈ s, f z ∈ Complex.slitPlane) :
HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by
let s₁ : Set ℂ := { z | f z ∈ Complex.slitPlane} ∩ s let s₁ : Set ℂ := { z | f z ∈ Complex.slitPlane} ∩ s
@ -269,7 +268,8 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
-- ∀ z ∈ s₁, f z ≠ 0 -- ∀ z ∈ s₁, f z ≠ 0
exact fun z hz ↦ h₂ z (Set.mem_of_mem_inter_right hz) exact fun z hz ↦ h₂ z (Set.mem_of_mem_inter_right hz)
-- ∀ z ∈ s₁, f z ∈ Complex.slitPlane -- ∀ z ∈ s₁, f z ∈ Complex.slitPlane
exact fun z hz ↦ h₃ z (Set.mem_of_mem_inter_right hz) intro z hz
apply hz.1
let s₂ : Set ℂ := { z | -f z ∈ Complex.slitPlane} ∩ s let s₂ : Set ℂ := { z | -f z ∈ Complex.slitPlane} ∩ s
@ -314,7 +314,19 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
rw [← this] rw [← this]
exact harm₁ exact harm₁
· use s₂ · use s₂
sorry constructor
· exact hs₂
· constructor
· tauto
· have : s₂ = s ∩ s₂ := by
apply Set.right_eq_inter.mpr
exact Set.inter_subset_right {z | -f z ∈ Complex.slitPlane} s
rw [← this]
have : Real.log ∘ ⇑Complex.normSq ∘ f = Real.log ∘ ⇑Complex.normSq ∘ (-f) := by
funext x
simp
rw [this]
exact harm₂
theorem log_normSq_of_holomorphic_is_harmonic theorem log_normSq_of_holomorphic_is_harmonic