IsLittleO
plain-language theorem explainer
IsLittleO encodes the classical little-o relation f = o(g) as x approaches a on the reals. Analysts and relativists in the Recognition framework cite it to replace informal error estimates with precise asymptotic predicates in limit statements. The definition is a direct predicate unfolding the epsilon-M condition with no lemmas or tactics required.
Claim. We write $f = o(g)$ as $x$ approaches $a$ when for every $ε > 0$ there exists $M > 0$ such that $|x - a| < M$ implies $|f(x)| ≤ ε |g(x)|$.
background
The module Relativity.Analysis.Limits integrates Mathlib asymptotics to supply rigorous O(·) and o(·) notation, replacing placeholder bounds with Filter-based definitions in the Recognition setting. Upstream, Recognition.M supplies the base structure with universe U and recognition map R; Cycle3.M instantiates it on a 3-cycle; as from ContinuumBridge identifies the Laplacian action on simplices via weighted edge sums equal to scaled defect terms.
proof idea
Direct definition. It encodes the predicate by quantifying over all ε > 0, then asserting existence of M > 0 such that the absolute-value inequality holds inside the M-neighborhood of a. No lemmas are invoked; the body is the standard little-o condition.
why it matters
IsLittleO is the base predicate for LandauCompositionFacts and for IsLittleOPower. It feeds the theorems littleO_implies_bigO and littleO_bigO_trans that convert little-o statements into big-O bounds. The definition supplies the rigorous limit language required for asymptotic analysis inside the Recognition framework's relativity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.