Compare commits

...

2 Commits

Author SHA1 Message Date
Stefan Kebekus 9d4657fb81 Update holomorphic_zero.lean 2024-08-16 15:20:24 +02:00
Stefan Kebekus 9ea3dcb2d6 Update holomorphic_zero.lean 2024-08-16 14:18:48 +02:00
1 changed files with 127 additions and 42 deletions

View File

@ -23,6 +23,15 @@ theorem analyticAtZeroDivisorSupport
simp [h₁f] at h simp [h₁f] at h
theorem zeroDivisor_eq_ord_AtZeroDivisorSupport
{f : }
{z : }
(h : z ∈ Function.support (zeroDivisor f)) :
zeroDivisor f z = (analyticAtZeroDivisorSupport h).order.toNat := by
unfold zeroDivisor
simp [analyticAtZeroDivisorSupport h]
lemma toNatEqSelf_iff {n : ℕ∞} : n.toNat = n ↔ ∃ m : , m = n := by lemma toNatEqSelf_iff {n : ℕ∞} : n.toNat = n ↔ ∃ m : , m = n := by
constructor constructor
· intro H₁ · intro H₁
@ -36,61 +45,122 @@ lemma toNatEqSelf_iff {n : ℕ∞} : n.toNat = n ↔ ∃ m : , m = n := by
simp simp
lemma natural_if_toNatNeZero {n : ℕ∞} : n.toNat ≠ 0 → ∃ m : , m = n := by
rw [← ENat.some_eq_coe, ← WithTop.ne_top_iff_exists]
contrapose; simp; tauto
theorem zeroDivisor_localDescription
{f : }
{z₀ : }
(h : z₀ ∈ Function.support (zeroDivisor f)) :
∃ (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
theorem discreteZeros theorem discreteZeros
{f : } : {f : } :
DiscreteTopology (Function.support (zeroDivisor f)) := by DiscreteTopology (Function.support (zeroDivisor f)) := by
apply singletons_open_iff_discrete.mp
simp_rw [← singletons_open_iff_discrete, Metric.isOpen_singleton_iff]
intro z intro z
let A := analyticAtZeroDivisorSupport z.2 have A : zeroDivisor f ↑z ≠ 0 := by exact z.2
let c : WithTop := A.order let B := zeroDivisor_eq_ord_AtZeroDivisorSupport z.2
let B := AnalyticAt.order_eq_nat_iff A rw [B] at A
let n := zeroDivisor f z.1 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 z.2) m
rw [E] at hm
obtain ⟨g, h₁g, h₂g, h₃g⟩ := hm
rw [Metric.eventually_nhds_iff_ball] at h₃g
have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑z) ε, g y ≠ 0 := by
have h₄g : ContinuousAt g z := AnalyticAt.continuousAt h₁g
have : {0}ᶜ ∈ nhds (g z) := by
exact compl_singleton_mem_nhds_iff.mpr h₂g
have : ∃ a : , a = A.order := by let F := h₄g.preimage_mem_nhds this
rw [← ENat.some_eq_coe] rw [Metric.mem_nhds_iff] at F
rw [← WithTop.ne_top_iff_exists] obtain ⟨ε, h₁ε, h₂ε⟩ := F
by_contra H use ε
rw [AnalyticAt.order_eq_top_iff] at H constructor; exact h₁ε
intro y hy
let G := h₂ε hy
simp at G
exact G
obtain ⟨ε₁, h₁ε₁⟩ := this
obtain ⟨ε₂, h₁ε₂, h₂ε₂⟩ := h₃g
use min ε₁ ε₂
constructor
· have : 0 < min ε₁ ε₂ := by
rw [lt_min_iff]
exact And.imp_right (fun _ => h₁ε₂) h₁ε₁
exact this
intro y
intro h₁y
dsimp [n, zeroDivisor] have h₂y : ↑y ∈ Metric.ball (↑z) ε₂ := by
simp [A] simp
calc dist y z
_ < min ε₁ ε₂ := by assumption
_ ≤ ε₂ := by exact min_le_right ε₁ ε₂
have h₃y : ↑y ∈ Metric.ball (↑z) ε₁ := by
simp
calc dist y z
_ < min ε₁ ε₂ := by assumption
_ ≤ ε₁ := by exact min_le_left ε₁ ε₂
let F := h₂ε₂ y.1 h₂y
rw [zeroDivisor_zeroSet y.2] at F
simp at F
simp [h₂m] at F
have : g y.1 ≠ 0 := by
sorry exact h₁ε₁.2 y h₃y
let C := (B n).1 this simp [this] at F
ext
apply Metric.isOpen_singleton_iff.mpr rwa [sub_eq_zero] at F
/-
Try this: refine Metric.isOpen_singleton_iff.mpr ?_
Remaining subgoals:
⊢ ∃ ε > 0, ∀ (y : ↑(Function.support (zeroDivisor f))), dist y z < ε → y = z
Suggestions
Try this: refine isClosed_compl_iff.mp ?_
Remaining subgoals:
⊢ IsClosed {z}ᶜ
Suggestions
Try this: refine disjoint_frontier_iff_isOpen.mp ?_
Remaining subgoals:
⊢ Disjoint (frontier {z}) {z}
Suggestions
Try this: refine isOpen_iff_forall_mem_open.mpr ?_
Remaining subgoals:
⊢ ∀ x ∈ {z}, ∃ t ⊆ {z}, IsOpen t ∧ x ∈ t
-/
sorry
theorem zeroDivisor_finiteOnCompact theorem zeroDivisor_finiteOnCompact
@ -105,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
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 sorry