IsBigOPower
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 in Recognition Science
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.
scope and limits
- Does not provide explicit values for the bounding constant or neighborhood radius.
- Does not apply to limits at infinity or at nonzero points.
- Does not imply the stronger little-o relation.
- Does not use Mathlib's Filter-based asymptotic library directly.
formal statement (Lean)
26def IsBigOPower (f : ℝ → ℝ) (n : ℕ) : Prop :=
proof body
Definition body.
27 IsBigO f (fun x => x ^ n) 0
28
29/-- f = o(x^n) as x → 0. -/