IsBigO
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not incorporate Mathlib's full Filter-based asymptotics.
- Does not define little-o notation.
- Does not handle composition with continuous functions without the LandauCompositionFacts class.
- Does not prove any inclusion or closure properties.
formal statement (Lean)
18def IsBigO (f g : ℝ → ℝ) (a : ℝ) : Prop :=
proof body
Definition body.
19 ∃ C > 0, ∃ M > 0, ∀ x, |x - a| < M → |f x| ≤ C * |g x|
20
21/-- Little-o notation: ∀ ε > 0, ∃ M such that |f(x)| ≤ ε|g(x)| for |x-a| < M. -/