littleO_implies_bigO
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.
claimIf 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 in Recognition Science
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.
scope and limits
- Does not supply explicit values for the constants C or M.
- Does not extend the relation to limits at infinity or to complex-valued functions.
- Does not address uniformity of the constants with respect to parameters.
formal statement (Lean)
129theorem littleO_implies_bigO (f g : ℝ → ℝ) (a : ℝ) :
130 IsLittleO f g a → IsBigO f g a := by
proof body
Term-mode proof.
131 intro h
132 -- Use ε = 1 to obtain a specific bound
133 have hε := h 1 (by norm_num : (0 : ℝ) < 1)
134 rcases hε with ⟨M, hMpos, hbound⟩
135 refine ⟨1, by norm_num, M, hMpos, ?_⟩
136 intro x hx
137 simpa using hbound x hx
138
139/-- f = o(g) and g = O(h) implies f = o(h). -/