Weighted Disk Argument Principle

Supporting definitions and lemmas for the Odlyzko-bound formalization.

noncomputable def NumberField.Odlyzko.fillFinitePunctures (f : ℂ → ℂ) (S : Finset ℂ) : ℂ → ℂ

A fill finite punctures used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.fillFinitePunctures f S z = if z ∈ S then (nhdsWithin z {z}ᶜ).limUnder f else f z

@[simp]

theorem NumberField.Odlyzko.fillFinitePunctures_apply_of_mem {f : ℂ → ℂ} {S : Finset ℂ} {z : ℂ} (hz : z ∈ S) : fillFinitePunctures f S z = (nhdsWithin z {z}ᶜ).limUnder f

@[simp]

theorem NumberField.Odlyzko.fillFinitePunctures_apply_of_notMem {f : ℂ → ℂ} {S : Finset ℂ} {z : ℂ} (hz : z ∉ S) : fillFinitePunctures f S z = f z

theorem NumberField.Odlyzko.fillFinitePunctures_eventuallyEq_nhdsNE (f : ℂ → ℂ) (S : Finset ℂ) (p : ℂ) : fillFinitePunctures f S =ᶠ[nhdsWithin p {p}ᶜ] f

theorem NumberField.Odlyzko.analyticAt_fillFinitePunctures_of_mem {f g : ℂ → ℂ} {S : Finset ℂ} {p : ℂ} (hp : p ∈ S) (hg : AnalyticAt ℂ g p) (hfg : f =ᶠ[nhdsWithin p {p}ᶜ] g) : AnalyticAt ℂ (fillFinitePunctures f S) p

theorem NumberField.Odlyzko.analyticAt_fillFinitePunctures_of_notMem {f : ℂ → ℂ} {S : Finset ℂ} {p : ℂ} (hp : p ∉ S) (hf : AnalyticAt ℂ f p) : AnalyticAt ℂ (fillFinitePunctures f S) p

noncomputable def NumberField.Odlyzko.weightedLogDerivFiniteRemainder (f h : ℂ → ℂ) (S : Finset ℂ) (order : ℂ → ℤ) : ℂ → ℂ

A weighted log deriv finite remainder used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.weightedLogDerivFiniteRemainder f h S order z = h z * logDeriv f z - ∑ p ∈ S, h p * ↑(order p) / (z - p)

theorem NumberField.Odlyzko.exists_analytic_weightedLogDerivFiniteRemainder_of_mem {f h : ℂ → ℂ} {S : Finset ℂ} {order : ℂ → ℤ} {p : ℂ} (hp : p ∈ S) (hf : MeromorphicAt f p) (horder : meromorphicOrderAt f p = ↑(order p)) (hh : AnalyticAt ℂ h p) : ∃ (g : ℂ → ℂ), AnalyticAt ℂ g p ∧ weightedLogDerivFiniteRemainder f h S order =ᶠ[nhdsWithin p {p}ᶜ] g

theorem NumberField.Odlyzko.analyticAt_weightedLogDerivFiniteRemainder_of_notMem {f h : ℂ → ℂ} {S : Finset ℂ} {order : ℂ → ℤ} {z : ℂ} (hz : z ∉ S) (hf : AnalyticAt ℂ f z) (hfz : f z ≠ 0) (hh : AnalyticAt ℂ h z) : AnalyticAt ℂ (weightedLogDerivFiniteRemainder f h S order) z

theorem NumberField.Odlyzko.analyticAt_fill_weightedLogDerivFiniteRemainder {f h : ℂ → ℂ} {S : Finset ℂ} {order : ℂ → ℤ} {z : ℂ} (hf : AnalyticAt ℂ f z) (hh : AnalyticAt ℂ h z) (hzero : f z = 0 → z ∈ S) (horder : ∀ p ∈ S, meromorphicOrderAt f p = ↑(order p)) : AnalyticAt ℂ (fillFinitePunctures (weightedLogDerivFiniteRemainder f h S order) S) z