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

Update holomorphic_zero.lean

This commit is contained in:
Stefan Kebekus 2024-08-18 19:47:10 +02:00
parent f9f177e7b9
commit 2c2370638a
1 changed files with 4 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
Nevanlinna/holomorphic_zero.lean
View File

@ -122,16 +122,14 @@ example
(h₁f : AnalyticOn ℂ f U) (h₁f : AnalyticOn ℂ f U)
(h₂f : ∃ z ∈ U, f z ≠ 0) : (h₂f : ∃ z ∈ U, f z ≠ 0) :
∀ (hz : z ∈ U), (h₁f z hz).order ≠ ⊤ := by ∀ (hz : z ∈ U), (h₁f z hz).order ≠ ⊤ := by
by_contra H by_contra H
push_neg at H push_neg at H
obtain ⟨z', hz'⟩ := H obtain ⟨z', hz'⟩ := H
rw [AnalyticAt.order_eq_top_iff] at hz' rw [AnalyticAt.order_eq_top_iff] at hz'
let A := AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' rw [← AnalyticAt.frequently_zero_iff_eventually_zero (h₁f z z')] at hz'
rw [AnalyticAt.frequently_eq_iff_eventually_eq] at A have A := AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' hz'
let B := A hz' tauto
sorry
theorem discreteZeros theorem discreteZeros