Working…

This commit is contained in:
Stefan Kebekus 2024-09-14 08:38:04 +02:00
parent 6610fd49b0
commit 12f0543f47
3 changed files with 150 additions and 5 deletions

View File

@ -3,6 +3,18 @@ import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Analytic.Linear
theorem AnalyticAt.order_neq_top_iff
{f : }
{z₀ : }
(hf : AnalyticAt f z₀) :
hf.order ≠ ↔ ∃ (g : ), AnalyticAt g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ) in nhds z₀, f z = (z - z₀) ^ (hf.order.toNat) • g z := by
rw [← hf.order_eq_nat_iff]
constructor
· intro h₁f
exact Eq.symm (ENat.coe_toNat h₁f)
· intro h₁f
exact ENat.coe_toNat_eq_self.mp (id (Eq.symm h₁f))
theorem AnalyticAt.order_mul
{f₁ f₂ : }

129
Nevanlinna/divisor.lean Normal file
View File

@ -0,0 +1,129 @@
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
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
simp
intro z hz
dsimp [AnalyticOn.zeroDivisor]
simp
tauto

View File

@ -1,15 +1,19 @@
import Mathlib.Analysis.Analytic.Meromorphic
import Nevanlinna.holomorphic_JensenFormula
open Real
variable {f : }
variable {h₁f : AnalyticOn f }
variable (f : )
variable {h₁f : MeromorphicOn f }
variable {h₂f : f 0 ≠ 0}
noncomputable def unintegratedCounting : := by
noncomputable def Nevanlinna.n : := by
intro r
let A := h₁f.mono (by tauto : Metric.closedBall (0 : ) r ⊆ )
exact ∑ᶠ z, (A.order z).toNat
have : MeromorphicAt f z := by
exact h₁f (sorryAx true) trivial
exact ∑ᶠ z ∈ Metric.ball (0 : ) r, (h₁f z trivial).order
noncomputable def integratedCounting : := by
intro r