IsBigOPower
plain-language theorem explainer
Big-O control of a real-valued function f by the monomial x^n near the origin is formalized here. Analysts establishing error controls for expansions in relativistic settings cite it to certify polynomial growth bounds. The definition consists of a direct reduction to the existential statement in the base big-O predicate applied at zero.
Claim. $f = O(x^n)$ as $x$ approaches 0, meaning there exist constants $C > 0$ and $M > 0$ such that $|f(x)|$ is at most $C$ times $|x^n|$ for all $x$ with $|x| < M$.
background
The module integrates Mathlib asymptotics to supply rigorous O and o notation, replacing placeholder error bounds with explicit definitions based on neighborhoods. The underlying big-O predicate at a point a asserts the existence of C > 0 and M > 0 such that |f(x)| ≤ C |g(x)| for all x satisfying |x - a| < M. This definition specializes that predicate by fixing the comparison function to the monomial x ↦ x^n and the point a to zero.
proof idea
This is a one-line definition that applies the big-O predicate to the monomial function x to the power n at the origin.
why it matters
The predicate is invoked in the proof that the square function satisfies the big-O relation with itself, confirming reflexivity of the bound. It equips the limits module with notation for asymptotic analysis in relativity, supporting bounds on error terms as the variable approaches zero. This closes a notational gap in the framework's treatment of local expansions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.