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

Update analyticOn_zeroSet.lean

This commit is contained in:
Stefan Kebekus 2024-08-20 17:27:42 +02:00
parent 867b88bf5a
commit 6d0870d533
1 changed files with 27 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
Nevanlinna/analyticOn_zeroSet.lean
View File

@ -380,14 +380,33 @@ theorem AnalyticOnCompact.eliminateZeros
obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
use g use g
use A use A
have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
intro z
rw [h₃g z]
congr
funext a
congr
dsimp [n]
simp [a.2]
constructor constructor
· exact h₁g · exact h₁g
· constructor · constructor
· sorry · intro z h₁z
· intro z by_cases h₂z : ⟨z, h₁z⟩ ∈ ↑A.toSet
rw [h₃g z] · exact h₂g ⟨z, h₁z⟩ h₂z
congr · have : f z ≠ 0 := by
funext a by_contra C
congr have : ⟨z, h₁z⟩ ∈ ↑A₁ := by
dsimp [n] dsimp [A₁, ι]
simp [a.2] simp
exact C
have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by
dsimp [A]
simp
exact this
tauto
rw [inter z] at this
exact right_ne_zero_of_smul this
· exact inter