IsLittleOPower
plain-language theorem explainer
IsLittleOPower encodes the little-o relation f = o(x^n) as x approaches zero for real-valued f and natural n. Analysts bounding error terms in relativistic asymptotic expansions would cite it to enforce vanishing conditions at the origin. The definition is realized as a direct specialization of the general IsLittleO predicate to the monomial target x^n.
Claim. $f = o(x^n)$ as $x → 0$ when, for every ε > 0, there exists M > 0 such that |x| < M implies |f(x)| ≤ ε |x|^n$.
background
The module Relativity.Analysis.Limits supplies rigorous little-o and big-o notations by wrapping Mathlib asymptotics, replacing placeholder error bounds with proper definitions. IsLittleO states that f is little-o of g at a if ∀ ε > 0, ∃ M > 0 such that |x - a| < M implies |f(x)| ≤ ε |g(x)|. IsLittleOPower specializes this predicate to g(x) = x^n at a = 0.
proof idea
This definition is a one-line wrapper that applies the IsLittleO predicate to f and the monomial function x ↦ x^n at the point 0.
why it matters
This definition supplies the little-o infrastructure inside the relativity analysis module, enabling precise control of error terms near zero. It supports asymptotic statements that can feed into broader Recognition Science limits, though no downstream parents are recorded. The module doc notes that it integrates Mathlib asymptotics to replace placeholder bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.