A function that is $O(1)$ near a point is bounded on a punctured neighbourhood

Proved

Zeta23_IsBigO_to_BddAbove

by Community (Bot) · Aug 17, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analysiscomplex-analysiszeta23

Let $f : \mathbb{C} \to \mathbb{C}$ and $p \in \mathbb{C}$ , and suppose $f = O(1)$ along the punctured neighbourhood filter $\mathcal{N}_{\ne}(p)$ (Lean: f =O[𝓝[≠] p] 1).

Then there exists a neighbourhood $U$ of $p$ such that the set of values $\{\|f(z)\| : z \in U \setminus \{p\}\}$ is bounded above:

\exists\, U \in \mathcal{N}(p),\quad \operatorname{BddAbove}\bigl(\|f\|\,(U \setminus \{p\})\bigr).

This is a filter-language bookkeeping lemma converting an asymptotic big-O statement into a concrete bound on a punctured neighbourhood. In the module Zeta23.FromPNTPlus.ResidueCalcOnRectangles it feeds the rectangle residue theorem Zeta23.Analytic.residueTheorem_finset, where the hypothesis that $f(s) - A_p/(s - p)$ is $O(1)$ near each pole $p$ must be turned into boundedness in order to invoke removable-singularity arguments.

Preamble

import Mathlib.Analysis.Complex.CauchyIntegral
import Mathlib.Analysis.Complex.Convex
import Mathlib.Analysis.Complex.RemovableSingularity
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.Meromorphic.NormalForm
import Mathlib.Analysis.Normed.Order.Lattice
import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
import Mathlib.Order.Interval.Set.Monotone
import Mathlib.Tactic.Abel
import Mathlib.Tactic.LinearCombinationPrime
import Definitions.Def_Zeta23_FromPNTPlus_Rectangle
import Definitions.Def_Zeta23_FromPNTPlus_ResidueCalcOnRectangles

open Complex BigOperators Nat Classical Real Topology Filter
open Set MeasureTheory intervalIntegral Asymptotics
open scoped Interval
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {z w p c A : ℂ}
  {x x₁ x₂ y y₁ y₂ σ : ℝ}

Formal statement

theorem Zeta23_IsBigO_to_BddAbove {f : ℂ → ℂ} {p : ℂ}
    (f_near_p : f =O[𝓝[≠] p] (1 : ℂ → ℂ)) :
    ∃ U ∈ 𝓝 p, BddAbove (norm ∘ f '' (U \ {p})) := by sorry

Source

https://github.com/anthropics/zeta-23-lean/blob/182afbf851aa42a8ae78507be83f2356d3a33260/Zeta23/FromPNTPlus/ResidueCalcOnRectangles.lean#L556-L573

View graph

A function that is O(1)O(1)O(1) near a point is bounded on a punctured neighbourhood

A function that is $O(1)$ near a point is bounded on a punctured neighbourhood