359 lines
9.5 KiB
Plaintext
359 lines
9.5 KiB
Plaintext
import Init.Classical
|
||
import Mathlib.Analysis.Analytic.Meromorphic
|
||
import Mathlib.Topology.ContinuousOn
|
||
import Mathlib.Analysis.Analytic.IsolatedZeros
|
||
import Nevanlinna.holomorphic
|
||
import Nevanlinna.analyticOn_zeroSet
|
||
|
||
|
||
noncomputable def zeroDivisor
|
||
(f : ℂ → ℂ) :
|
||
ℂ → ℕ := by
|
||
intro z
|
||
by_cases hf : AnalyticAt ℂ f z
|
||
· exact hf.order.toNat
|
||
· exact 0
|
||
|
||
|
||
theorem analyticAtZeroDivisorSupport
|
||
{f : ℂ → ℂ}
|
||
{z : ℂ}
|
||
(h : z ∈ Function.support (zeroDivisor f)) :
|
||
AnalyticAt ℂ f z := by
|
||
|
||
by_contra h₁f
|
||
simp at h
|
||
dsimp [zeroDivisor] 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]
|
||
|
||
|
||
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₁
|
||
rw [← ENat.some_eq_coe, ← WithTop.ne_top_iff_exists]
|
||
by_contra H₂
|
||
rw [H₂] at H₁
|
||
simp at H₁
|
||
· intro H
|
||
obtain ⟨m, hm⟩ := H
|
||
rw [← hm]
|
||
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 zeroDivisor_support_iff
|
||
{f : ℂ → ℂ}
|
||
{z₀ : ℂ} :
|
||
z₀ ∈ Function.support (zeroDivisor f) ↔
|
||
f z₀ = 0 ∧
|
||
AnalyticAt ℂ f z₀ ∧
|
||
∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ (zeroDivisor f z₀) • g z := by
|
||
constructor
|
||
· intro hz
|
||
constructor
|
||
· exact zeroDivisor_zeroSet hz
|
||
· constructor
|
||
· exact analyticAtZeroDivisorSupport hz
|
||
· exact zeroDivisor_localDescription hz
|
||
· intro ⟨h₁, h₂, h₃⟩
|
||
have : zeroDivisor f z₀ = (h₂.order).toNat := by
|
||
unfold zeroDivisor
|
||
simp [h₂]
|
||
simp [this]
|
||
simp [(h₂.order_eq_nat_iff (zeroDivisor f z₀)).2 h₃]
|
||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := h₃
|
||
rw [Filter.Eventually.self_of_nhds h₃g] at h₁
|
||
simp [h₂g] at h₁
|
||
assumption
|
||
|
||
|
||
theorem topOnPreconnected
|
||
{f : ℂ → ℂ}
|
||
{U : Set ℂ}
|
||
(hU : IsPreconnected U)
|
||
(h₁f : AnalyticOn ℂ f U)
|
||
(h₂f : ∃ z ∈ U, f z ≠ 0) :
|
||
∀ (hz : z ∈ U), (h₁f z hz).order ≠ ⊤ := by
|
||
|
||
by_contra H
|
||
push_neg at H
|
||
obtain ⟨z', hz'⟩ := H
|
||
rw [AnalyticAt.order_eq_top_iff] at hz'
|
||
rw [← AnalyticAt.frequently_zero_iff_eventually_zero (h₁f z z')] at hz'
|
||
have A := AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' hz'
|
||
tauto
|
||
|
||
|
||
theorem supportZeroSet
|
||
{f : ℂ → ℂ}
|
||
{U : Set ℂ}
|
||
(hU : IsPreconnected U)
|
||
(h₁f : AnalyticOn ℂ f U)
|
||
(h₂f : ∃ z ∈ U, f z ≠ 0) :
|
||
U ∩ Function.support (zeroDivisor f) = U ∩ f⁻¹' {0} := by
|
||
|
||
ext x
|
||
constructor
|
||
· intro hx
|
||
constructor
|
||
· exact hx.1
|
||
exact zeroDivisor_zeroSet hx.2
|
||
· simp
|
||
intro h₁x h₂x
|
||
constructor
|
||
· exact h₁x
|
||
· let A := zeroDivisor_support_iff (f := f) (z₀ := x)
|
||
simp at A
|
||
rw [A]
|
||
constructor
|
||
· exact h₂x
|
||
· constructor
|
||
· exact h₁f x h₁x
|
||
· have B := AnalyticAt.order_eq_nat_iff (h₁f x h₁x) (zeroDivisor f x)
|
||
simp at B
|
||
rw [← B]
|
||
dsimp [zeroDivisor]
|
||
simp [h₁f x h₁x]
|
||
refine Eq.symm (ENat.coe_toNat ?h.mpr.right.right.right.a)
|
||
exact topOnPreconnected hU h₁f h₂f h₁x
|
||
|
||
|
||
theorem discreteZeros
|
||
{f : ℂ → ℂ} :
|
||
DiscreteTopology (Function.support (zeroDivisor f)) := by
|
||
|
||
simp_rw [← singletons_open_iff_discrete, Metric.isOpen_singleton_iff]
|
||
intro z
|
||
|
||
have A : zeroDivisor f ↑z ≠ 0 := by exact z.2
|
||
let B := zeroDivisor_eq_ord_AtZeroDivisorSupport z.2
|
||
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 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
|
||
|
||
let F := h₄g.preimage_mem_nhds this
|
||
rw [Metric.mem_nhds_iff] at F
|
||
obtain ⟨ε, h₁ε, h₂ε⟩ := F
|
||
use ε
|
||
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
|
||
|
||
have h₂y : ↑y ∈ Metric.ball (↑z) ε₂ := by
|
||
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
|
||
exact h₁ε₁.2 y h₃y
|
||
simp [this] at F
|
||
ext
|
||
rwa [sub_eq_zero] at F
|
||
|
||
|
||
theorem zeroDivisor_finiteOnCompact
|
||
{f : ℂ → ℂ}
|
||
{U : Set ℂ}
|
||
(hU : IsPreconnected U)
|
||
(h₁f : AnalyticOn ℂ f U)
|
||
(h₂f : ∃ z ∈ U, f z ≠ 0) -- not needed!
|
||
(h₂U : IsCompact U) :
|
||
Set.Finite (U ∩ Function.support (zeroDivisor f)) := by
|
||
|
||
have hinter : IsCompact (U ∩ Function.support (zeroDivisor f)) := by
|
||
apply IsCompact.of_isClosed_subset h₂U
|
||
rw [supportZeroSet]
|
||
apply h₁f.continuousOn.preimage_isClosed_of_isClosed
|
||
exact IsCompact.isClosed h₂U
|
||
exact isClosed_singleton
|
||
assumption
|
||
assumption
|
||
assumption
|
||
exact Set.inter_subset_left
|
||
|
||
apply hinter.finite
|
||
apply DiscreteTopology.of_subset (s := Function.support (zeroDivisor f))
|
||
exact discreteZeros (f := f)
|
||
exact Set.inter_subset_right
|
||
|
||
|
||
|
||
|
||
noncomputable def zeroDivisorDegree
|
||
{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!
|
||
ℕ := (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
|
||
|
||
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
|
||
|
||
-- 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 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
|
||
· assumption
|
||
·
|
||
sorry
|