Update holomorphic_zero.lean

This commit is contained in:
Stefan Kebekus 2024-08-19 14:08:00 +02:00
parent ec79ed7ba1
commit a910bd6988
1 changed files with 70 additions and 36 deletions

View File

@ -36,6 +36,17 @@ theorem zeroDivisor_eq_ord_AtZeroDivisorSupport
simp [analyticAtZeroDivisorSupport h]
theorem zeroDivisor_eq_ord_AtZeroDivisorSupport'
{f : }
{z : }
(h : z ∈ Function.support (zeroDivisor f)) :
zeroDivisor f z = (analyticAtZeroDivisorSupport h).order := by
unfold zeroDivisor
simp [analyticAtZeroDivisorSupport h]
sorry
lemma toNatEqSelf_iff {n : ℕ∞} : n.toNat = n ↔ ∃ m : , m = n := by
constructor
· intro H₁
@ -338,52 +349,75 @@ theorem AnalyticOn.order_eq_nat_iff
tauto
theorem eliminatingZeros
noncomputable def zeroDivisorDegree
{f : }
{U : Set }
(h₁U : IsPreconnected U)
(h₁U : IsPreconnected U) -- not needed!
(h₂U : IsCompact U)
(h₁f : AnalyticOn f U)
(h₂f : ∃ z ∈ U, f z ≠ 0) :
(h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed!
:= (zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U).toFinset.card
lemma zeroDivisorDegreeZero
{f : }
{U : Set }
(h₁U : IsPreconnected U) -- not needed!
(h₂U : IsCompact U)
(h₁f : AnalyticOn f U)
(h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed!
0 = zeroDivisorDegree h₁U h₂U h₁f h₂f ↔ U ∩ (zeroDivisor f).support = ∅ := by
sorry
lemma eliminatingZeros₀
{U : Set }
(h₁U : IsPreconnected U)
(h₂U : IsCompact U) :
∀ n : , ∀ f : , (h₁f : AnalyticOn f U) → (h₂f : ∃ z ∈ U, f z ≠ 0) →
(n = zeroDivisorDegree h₁U h₂U h₁f h₂f) →
∃ F : , (AnalyticOn F U) ∧ (f = F * ∏ᶠ a ∈ (U ∩ (zeroDivisor f).support), fun z ↦ (z - a) ^ (zeroDivisor f a)) := by
have hs := zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U
rw [finprod_mem_eq_finite_toFinset_prod _ hs]
intro n
induction' n with n ih
-- case zero
intro f h₁f h₂f h₃f
use f
rw [zeroDivisorDegreeZero] at h₃f
rw [h₃f]
simpa
let A := hs.card_eq
-- case succ
intro f h₁f h₂f h₃f
let Supp := (zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U).toFinset
have : Supp.Nonempty := by
rw [← Finset.one_le_card]
calc 1
_ ≤ n + 1 := by exact Nat.le_add_left 1 n
_ = zeroDivisorDegree h₁U h₂U h₁f h₂f := by exact h₃f
_ = Supp.card := by rfl
obtain ⟨z₀, hz₀⟩ := this
dsimp [Supp] at hz₀
simp only [Set.Finite.mem_toFinset, Set.mem_inter_iff] at hz₀
let F : := by
intro z
if hz : z ∈ U ∩ (zeroDivisor f).support then
exact (Classical.choose (zeroDivisor_support_iff.1 hz.2).2.2) z
else
exact (f z) / ∏ i ∈ hs.toFinset, (z - i) ^ zeroDivisor f i
let A := AnalyticOn.order_eq_nat_iff h₁f hz₀.1 (zeroDivisor f z₀)
let B := zeroDivisor_eq_ord_AtZeroDivisorSupport hz₀.2
let B := zeroDivisor_eq_ord_AtZeroDivisorSupport' hz₀.2
rw [eq_comm] at B
let C := A B
obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := C
have h₄g₀ : ∃ z ∈ U, g₀ z ≠ 0 := by sorry
have h₅g₀ : n = zeroDivisorDegree h₁U h₂U h₁g₀ h₄g₀ := by sorry
obtain ⟨F, h₁F, h₂F⟩ := ih g₀ h₁g₀ h₄g₀ h₅g₀
use F
constructor
· intro z h₁z
by_cases h₂z : z ∈ (zeroDivisor f).support
· -- case: z ∈ Function.support (zeroDivisor f)
have : z ∈ U ∩ (zeroDivisor f).support := by exact Set.mem_inter h₁z h₂z
sorry
· sorry
have : MeromorphicOn F U := by
apply MeromorphicOn.div
exact AnalyticOn.meromorphicOn h₁f
apply AnalyticOn.meromorphicOn
apply Finset.analyticOn_prod
intro n hn
apply AnalyticOn.pow
apply AnalyticOn.sub
exact analyticOn_id
exact analyticOn_const
--use F
· assumption
·
sorry