140 lines
3.7 KiB
Plaintext
140 lines
3.7 KiB
Plaintext
import Nevanlinna.analyticAt
|
||
|
||
|
||
structure Divisor where
|
||
toFun : ℂ → ℤ
|
||
discreteSupport : DiscreteTopology (Function.support toFun)
|
||
|
||
instance : CoeFun Divisor (fun _ ↦ ℂ → ℤ) where
|
||
coe := Divisor.toFun
|
||
attribute [coe] Divisor.toFun
|
||
|
||
|
||
|
||
noncomputable def Divisor.deg
|
||
(D : Divisor) : ℤ := ∑ᶠ z, D z
|
||
|
||
noncomputable def Divisor.n_trunk
|
||
(D : Divisor) : ℤ → ℝ → ℤ := fun k r ↦ ∑ᶠ z ∈ Metric.ball 0 r, min k (D z)
|
||
|
||
noncomputable def Divisor.n
|
||
(D : Divisor) : ℝ → ℤ := fun r ↦ ∑ᶠ z ∈ Metric.ball 0 r, D z
|
||
|
||
noncomputable def Divisor.N_trunk
|
||
(D : Divisor) : ℤ → ℝ → ℝ := fun k r ↦ ∫ (t : ℝ) in (1)..r, (D.n_trunk k t) / t
|
||
|
||
theorem Divisor.compactSupport
|
||
(D : Divisor)
|
||
{U : Set ℂ}
|
||
(h₁U : IsCompact U)
|
||
(h₂U : Function.support D ⊆ U) :
|
||
Set.Finite (Function.support D) := by
|
||
sorry
|
||
|
||
|
||
noncomputable def AnalyticOn.zeroDivisor
|
||
{f : ℂ → ℂ}
|
||
{U : Set ℂ}
|
||
(hf : AnalyticOn ℂ f U) :
|
||
Divisor where
|
||
|
||
toFun := by
|
||
intro z
|
||
if hz : z ∈ U then
|
||
exact ((hf z hz).order.toNat : ℤ)
|
||
else
|
||
exact 0
|
||
|
||
discreteSupport := by
|
||
simp_rw [← singletons_open_iff_discrete]
|
||
simp_rw [Metric.isOpen_singleton_iff]
|
||
simp
|
||
|
||
-- simp only [dite_eq_ite, gt_iff_lt, Subtype.forall, Function.mem_support, ne_eq, ite_eq_else, Classical.not_imp, not_or, Subtype.mk.injEq]
|
||
|
||
intro a ha ⟨h₁a, h₂a⟩
|
||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (AnalyticAt.order_neq_top_iff (hf a ha)).1 h₂a
|
||
rw [Metric.eventually_nhds_iff_ball] at h₃g
|
||
|
||
have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑a) ε, g y ≠ 0 := by
|
||
have h₄g : ContinuousAt g a :=
|
||
AnalyticAt.continuousAt h₁g
|
||
have : {0}ᶜ ∈ nhds (g a) := 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 hy ⟨h₁y, h₂y⟩ h₃
|
||
|
||
have h'₂y : ↑y ∈ Metric.ball (↑a) ε₂ := by
|
||
simp
|
||
calc dist y a
|
||
_ < min ε₁ ε₂ := by assumption
|
||
_ ≤ ε₂ := by exact min_le_right ε₁ ε₂
|
||
|
||
have h₃y : ↑y ∈ Metric.ball (↑a) ε₁ := by
|
||
simp
|
||
calc dist y a
|
||
_ < min ε₁ ε₂ := by assumption
|
||
_ ≤ ε₁ := by exact min_le_left ε₁ ε₂
|
||
|
||
have F := h₂ε₂ y h'₂y
|
||
have : f y = 0 := by
|
||
rw [AnalyticAt.order_eq_zero_iff (hf y hy)] at h₁y
|
||
tauto
|
||
rw [this] at F
|
||
simp at F
|
||
|
||
have : g y ≠ 0 := by
|
||
exact h₁ε₁.2 y h₃y
|
||
simp [this] at F
|
||
rw [sub_eq_zero] at F
|
||
tauto
|
||
|
||
|
||
theorem AnalyticOn.support_of_zeroDivisor
|
||
{f : ℂ → ℂ}
|
||
{U : Set ℂ}
|
||
(hf : AnalyticOn ℂ f U) :
|
||
Function.support hf.zeroDivisor ⊆ U := by
|
||
|
||
intro z
|
||
contrapose
|
||
intro hz
|
||
dsimp [AnalyticOn.zeroDivisor]
|
||
simp
|
||
tauto
|
||
|
||
|
||
theorem AnalyticOn.support_of_zeroDivisor₂
|
||
{f : ℂ → ℂ}
|
||
{U : Set ℂ}
|
||
(hf : AnalyticOn ℂ f U) :
|
||
Function.support hf.zeroDivisor ⊆ f⁻¹' {0} := by
|
||
|
||
intro z hz
|
||
dsimp [AnalyticOn.zeroDivisor] at hz
|
||
have t₀ := hf.support_of_zeroDivisor hz
|
||
simp [hf.support_of_zeroDivisor hz] at hz
|
||
let A := hz.1
|
||
let C := (hf z t₀).order_eq_zero_iff
|
||
simp
|
||
rw [C] at A
|
||
tauto
|