IsLittleOPower
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 in Recognition Science
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.
scope and limits
- Does not extend the condition to limits at infinity or points other than zero.
- Does not supply explicit rates or constants beyond the existential definition.
- Does not reference J-cost, phi-ladder, or forcing-chain structures.
formal statement (Lean)
30def IsLittleOPower (f : ℝ → ℝ) (n : ℕ) : Prop :=
proof body
Definition body.
31 IsLittleO f (fun x => x ^ n) 0
32
33/-- Constant function is O(1). -/