Source indexedlemma · leanprover/lean4:v4.32.0

CH2.meromorphicOrderAt_nonneg_of_eventually_bounded

PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3510 to 3518

Source documentation

If f is bounded on a punctured neighborhood of z, its meromorphic order there is ≥ 0. (If f is not meromorphic at z the order is the junk value 0; otherwise a negative order would force f → ∞, contradicting the bound.)

Exact Lean statement

lemma meromorphicOrderAt_nonneg_of_eventually_bounded {f : ℂ → ℂ} {z : ℂ} {M : ℝ}
    (hbdd : ∀ᶠ s in nhdsWithin z {z}ᶜ, ‖f s‖ ≤ M) : 0 ≤ meromorphicOrderAt f z

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma meromorphicOrderAt_nonneg_of_eventually_bounded {f : ℂ → ℂ} {z : ℂ} {M : ℝ}    (hbdd : ∀ᶠ s in nhdsWithin z {z}ᶜ, ‖f s‖ ≤ M) : 0 ≤ meromorphicOrderAt f z := by  by_cases hmero : MeromorphicAt f z  · rw [← not_lt, ← tendsto_cobounded_iff_meromorphicOrderAt_neg hmero,      ← tendsto_norm_atTop_iff_cobounded]    intro htend    obtain ⟨s, hs1, hs2⟩ := ((htend.eventually_gt_atTop M).and hbdd).exists    exact absurd hs1 (not_lt.mpr hs2)  · rw [meromorphicOrderAt_of_not_meromorphicAt hmero]