IsLittleO
IsLittleO encodes the classical little-o relation f = o(g) as x approaches a on the reals. Analysts and relativists in the Recognition framework cite it to replace informal error estimates with precise asymptotic predicates in limit statements. The definition is a direct predicate unfolding the epsilon-M condition with no lemmas or tactics required.
claimWe write $f = o(g)$ as $x$ approaches $a$ when for every $ε > 0$ there exists $M > 0$ such that $|x - a| < M$ implies $|f(x)| ≤ ε |g(x)|$.
background
The module Relativity.Analysis.Limits integrates Mathlib asymptotics to supply rigorous O(·) and o(·) notation, replacing placeholder bounds with Filter-based definitions in the Recognition setting. Upstream, Recognition.M supplies the base structure with universe U and recognition map R; Cycle3.M instantiates it on a 3-cycle; as from ContinuumBridge identifies the Laplacian action on simplices via weighted edge sums equal to scaled defect terms.
proof idea
Direct definition. It encodes the predicate by quantifying over all ε > 0, then asserting existence of M > 0 such that the absolute-value inequality holds inside the M-neighborhood of a. No lemmas are invoked; the body is the standard little-o condition.
why it matters in Recognition Science
IsLittleO is the base predicate for LandauCompositionFacts and for IsLittleOPower. It feeds the theorems littleO_implies_bigO and littleO_bigO_trans that convert little-o statements into big-O bounds. The definition supplies the rigorous limit language required for asymptotic analysis inside the Recognition framework's relativity module.
scope and limits
- Does not assume continuity or differentiability of f or g.
- Does not extend beyond real-valued functions on the real line.
- Does not incorporate Mathlib Filter.atTop or other non-metric filters.
- Does not guarantee existence of explicit computable M for given ε.
formal statement (Lean)
22def IsLittleO (f g : ℝ → ℝ) (a : ℝ) : Prop :=
proof body
Definition body.
23 ∀ ε > 0, ∃ M > 0, ∀ x, |x - a| < M → |f x| ≤ ε * |g x|
24
25/-- f = O(x^n) as x → 0. -/