OAI/NumberTheory/Ostmann/ZeroDensity/FiniteZeroQuotientDisk.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.finiteZeroPolynomial_norm_le line 13
2. theorem OAI.Ostmann.finiteZeroPolynomial_norm_ge line 21
3. theorem OAI.Ostmann.finite_zero_quotient_disk_bound line 31

   Source documentation

   The annulus between radii 2R and 3R separates the removed zeros from the circle on which the original function is estimated.

   theorem finite_zero_quotient_disk_bound (f g : ℂ → ℂ) (S : Finset ℂ)
       (R M : ℝ) (hR : 0 < R) (_hM : 0 ≤ M)
       (hS : ∀ w ∈ S, ‖w‖ ≤ 2 * R)
       (hg : ∀ s, AnalyticAt ℂ g s)
       (he : ∀ s, f s = finiteZeroPolynomial f S s * g s)
       (hf : ∀ z ∈ sphere (0 : ℂ) (3 * R), ‖f z‖ ≤ M) :
       ∀ z ∈ closedBall (0 : ℂ) (3 * R),
         ‖g z‖ ≤ M / R ^ (∑ w ∈ S, analyticOrderNatAt f w) := by
   …

   Mentions: OAI.Ostmann.finiteZeroPolynomial