IsBigO
plain-language theorem explainer
Big-O notation is defined as the existence of positive constants C and M such that |f(x)| is bounded by C times |g(x)| for all x sufficiently close to a. Analysts working on error bounds in the Recognition Science relativity module cite this definition when controlling asymptotic expansions. The definition is supplied directly by the existential quantifiers without invoking any lemmas.
Claim. The function $f$ is big-O of $g$ at the point $a$ when there exist constants $C>0$ and $M>0$ such that $|x-a|<M$ implies $|f(x)|$ is at most $C$ times $|g(x)|$.
background
The module supplies limits and asymptotic analysis that integrates with Mathlib to replace placeholder error bounds with rigorous O and o notation. The definition sits inside the Recognition framework's analytic layer, where functions from reals to reals appear in lattice sums and cycle structures. Upstream structures include the meta-realization cert recording structural properties for self-reference axioms and the phi-ladder Poisson summation hypothesis that can be assumed until analytic infrastructure is discharged.
proof idea
The definition is given directly by the existential statement matching the classical big-O condition. No lemmas are applied; it serves as the base predicate for all subsequent theorems in the module.
why it matters
This supplies the core notation for the Landau facts, including bigO_add_subset showing O(f) plus O(g) contained in O of the pointwise max, bigO_const_mul for scalar multiplication, and bigO_mul_subset. It fills the asymptotic bound role needed for phi-ladder lattice sums and cycle-3 recognition structures. The definition touches the open question of discharging the analytic hypotheses once full infrastructure arrives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.