littleO_implies_bigO
plain-language theorem explainer
Little-o notation implies big-O notation for real-valued functions near a point. Analysts working with asymptotic error bounds in relativity would cite this when converting strict little-o estimates into usable big-O controls. The proof extracts a concrete constant by specializing the epsilon quantifier to 1 and reusing the resulting neighborhood bound.
Claim. If for functions $f,g:ℝ→ℝ$ and point $a∈ℝ$, for every $ε>0$ there exists $M>0$ such that $|x-a|<M$ implies $|f(x)|≤ε|g(x)|$, then there exist $C>0$ and $M>0$ such that $|x-a|<M$ implies $|f(x)|≤C|g(x)|$.
background
The module supplies Filter-based replacements for placeholder error bounds, defining little-o as the statement that for every positive ε a neighborhood exists in which |f| is bounded by ε times |g|. Big-O is the weaker existential claim that some fixed positive C and neighborhood suffice for the same inequality with C in place of ε. These sit inside the Limits submodule of Relativity.Analysis and draw on the Recognition structure M together with cycle and phase-lift auxiliaries for downstream applications.
proof idea
The proof introduces the little-o hypothesis, instantiates it at ε=1 to obtain a concrete positive M and bound, then packages the big-O witness with C=1 and the same M; the final inequality follows by direct simplification of the bound.
why it matters
The result records the standard inclusion of little-o inside big-O, supplying a basic relation that supports tighter control of approximations inside the Recognition framework's relativity limits. It belongs to the same module that defines addition, multiplication, and composition rules for big-O, thereby closing a small fragment of the asymptotic toolkit needed for error propagation along the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.