Update holomorphic_zero.lean

This commit is contained in:
Stefan Kebekus 2024-08-16 15:20:24 +02:00
parent 9ea3dcb2d6
commit 9d4657fb81
1 changed files with 53 additions and 8 deletions

View File

@ -50,13 +50,43 @@ lemma natural_if_toNatNeZero {n : ℕ∞} : n.toNat ≠ 0 → ∃ m : , m = n
contrapose; simp; tauto contrapose; simp; tauto
theorem zeroDivisor_in_zeroSet theorem zeroDivisor_localDescription
{f : } {f : }
{z : } {z₀ : }
(h : z ∈ Function.support (zeroDivisor f)) : (h : z₀ ∈ Function.support (zeroDivisor f)) :
f z = 0 := by ∃ (g : ), AnalyticAt g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ) in nhds z₀, f z = (z - z₀) ^ (zeroDivisor f z₀) • g z := by
have A : zeroDivisor f ↑z₀ ≠ 0 := by exact h
let B := zeroDivisor_eq_ord_AtZeroDivisorSupport h
rw [B] at A
have C := natural_if_toNatNeZero A
obtain ⟨m, hm⟩ := C
have h₂m : m ≠ 0 := by
rw [← hm] at A
simp at A
assumption
rw [eq_comm] at hm
let E := AnalyticAt.order_eq_nat_iff (analyticAtZeroDivisorSupport h) m
let F := hm
rw [E] at F
have : m = zeroDivisor f z₀ := by
rw [B, hm]
simp
rwa [this] at F
theorem zeroDivisor_zeroSet
{f : }
{z₀ : }
(h : z₀ ∈ Function.support (zeroDivisor f)) :
f z₀ = 0 := by
obtain ⟨g, _, _, h₃⟩ := zeroDivisor_localDescription h
rw [Filter.Eventually.self_of_nhds h₃]
simp
left
exact h
sorry
theorem discreteZeros theorem discreteZeros
{f : } : {f : } :
@ -121,7 +151,7 @@ theorem discreteZeros
_ ≤ ε₁ := by exact min_le_left ε₁ ε₂ _ ≤ ε₁ := by exact min_le_left ε₁ ε₂
let F := h₂ε₂ y.1 h₂y let F := h₂ε₂ y.1 h₂y
rw [zeroDivisor_in_zeroSet y.2] at F rw [zeroDivisor_zeroSet y.2] at F
simp at F simp at F
simp [h₂m] at F simp [h₂m] at F
@ -145,7 +175,22 @@ theorem eliminatingZeros
{f : } {f : }
{z₀ : } {z₀ : }
{R : } {R : }
(h₁f : ∀ z ∈ Metric.ball z₀ R, HolomorphicAt f z) (h₁f : ∀ z ∈ Metric.closedBall z₀ R, HolomorphicAt f z)
(h₂f : ∃ z ∈ Metric.ball z₀ R, f z ≠ 0) : (h₂f : ∃ z ∈ Metric.ball z₀ R, f z ≠ 0) :
∃ F : , ∀ z ∈ Metric.ball z₀ R, (HolomorphicAt F z) ∧ (f z = (F z) * ∏ᶠ a ∈ Metric.ball z₀ R, (z - a) ^ (zeroDivisor f a) ) := by ∃ F : , ∀ z ∈ Metric.ball z₀ R, (HolomorphicAt F z) ∧ (f z = (F z) * ∏ᶠ a ∈ Metric.ball z₀ R, (z - a) ^ (zeroDivisor f a) ) := by
sorry
let F : := by
intro z
if hz : z ∈ (Metric.closedBall z₀ R) ∩ Function.support (zeroDivisor f) then
exact 0
else
exact f z * (∏ᶠ a ∈ Metric.ball z₀ R, (z - a) ^ (zeroDivisor f a))⁻¹
use F
intro z hz
by_cases h₂z : z ∈ (Metric.closedBall z₀ R) ∩ Function.support (zeroDivisor f)
· -- Positive case
sorry
· -- Negative case
sorry