OAI/NumberTheory/Ostmann/ZeroDensity/FiniteAnalyticZeroFactors.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.finiteZeroPolynomial line 12
2. theorem OAI.Ostmann.finiteZeroPolynomial_analytic line 16
3. theorem OAI.Ostmann.finiteZeroPolynomial_ne_zero line 20
4. theorem OAI.Ostmann.finiteZeroPolynomial_insert line 26
5. theorem OAI.Ostmann.remove_finite_analytic_zeros line 34

   Source documentation

   The quotient by any finite collection of complete zero factors extends analytically to the whole plane. It is nonzero at each removed zero.

   theorem remove_finite_analytic_zeros (f : ℂ → ℂ)
       (hf : ∀ z, AnalyticAt ℂ f z) (horder : ∀ z, analyticOrderAt f z ≠ ⊤) (S : Finset ℂ) :
       ∃ g : ℂ → ℂ, (∀ s, AnalyticAt ℂ g s) ∧
         (∀ s, f s = finiteZeroPolynomial f S s * g s) ∧
         (∀ s ∈ S, g s ≠ 0) := by
   …

   Mentions: OAI.Ostmann.finiteZeroPolynomial