littleO_bigO_trans
plain-language theorem explainer
If f is little-o of g at a and g is big-O of h at a then f is little-o of h at a. Analysts chaining asymptotic error bounds in relativistic models cite this to compose limits without losing the little-o strictness. The tactic proof rescales the epsilon from the little-o hypothesis by the constant C extracted from big-O, takes the minimum of the two neighborhood radii, and chains the resulting inequalities via le_trans and ring normalization.
Claim. If $f=o(g)$ as $x→a$ and $g=O(h)$ as $x→a$, then $f=o(h)$ as $x→a$, where $f=o(g)$ means that for every $ε>0$ there exists $M>0$ such that $|x-a|<M$ implies $|f(x)|≤ε|g(x)|$, and $g=O(h)$ means there exist $C>0$ and $M>0$ such that $|x-a|<M$ implies $|g(x)|≤C|h(x)|$.
background
IsLittleO f g a is the definition asserting that for every positive ε there is a positive M such that |x-a|<M forces |f x| ≤ ε |g x|. IsBigO g h a asserts existence of positive C and M such that |g x| ≤ C |h x| holds in the same punctured neighborhood. The module integrates Mathlib asymptotics to replace placeholder error bounds with these Filter-based notations.
proof idea
The tactic proof introduces the two hypotheses, extracts C and M2 from the big-O assumption, defines ε' := ε/C, obtains M1 from the little-o assumption at ε', forms the min of M1 and M2, and then shows |f x| ≤ ε' |g x| ≤ ε' C |h x| = ε |h x| inside the smaller neighborhood by applying mul_le_mul_of_nonneg_left, le_trans, and ring normalization.
why it matters
The lemma supplies the basic transitivity needed to chain asymptotic relations once placeholder bounds are replaced by rigorous little-o and big-O in the Limits module. It supports composition of error estimates in relativistic analysis without dropping to big-O. No downstream uses are recorded yet, but the result closes a standard gap in the asymptotic toolkit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.