x_squared_is_O_x_squared
The declaration establishes that the map x to x squared satisfies big-O of x to the power 2 as x approaches zero. Analysts deriving error bounds for quadratic terms in relativistic limits would cite this reflexive case to anchor asymptotic estimates. The proof unfolds the power and big-O definitions then exhibits the trivial constant bound of one via norm_num and simplification.
claimThe function $f(x) = x^2$ satisfies $f = O(x^2)$ as $x → 0$.
background
The module integrates Mathlib asymptotics to replace placeholder error bounds with Filter-based definitions for limits in relativity analysis. IsBigO f g a asserts existence of C > 0 and M > 0 such that |x - a| < M implies |f x| ≤ C |g x|. IsBigOPower f n is defined as IsBigO f (x ↦ x^n) at the point 0, so the notation f = O(x^n) as x → 0 is captured exactly by this predicate.
proof idea
The tactic proof unfolds IsBigOPower and IsBigO, then refines the existential quantifiers by supplying C = 1, M = 1 and the trivial inequality. After the intro x step, simpa closes the bound |x^2| ≤ 1 · |x^2|.
why it matters in Recognition Science
This reflexive instance supplies a base case for quadratic error terms inside the relativity analysis module. It anchors the integration of Mathlib asymptotics into Recognition Science limit handling, ensuring that subsequent big-O manipulations rest on verified definitions rather than informal notation. No downstream uses are recorded, yet the result closes the trivial power case required for any chain of asymptotic estimates.
scope and limits
- Does not establish the corresponding little-o statement.
- Does not address the limit as x → ∞.
- Does not supply non-trivial constants or decay rates.
- Does not extend to functions other than x ↦ x^2.
formal statement (Lean)
58theorem x_squared_is_O_x_squared :
59 IsBigOPower (fun x => x ^ 2) 2 := by
proof body
Tactic-mode proof.
60 unfold IsBigOPower IsBigO
61 refine ⟨1, by norm_num, 1, by norm_num, ?_⟩
62 intro x _
63 have : |(x ^ 2)| ≤ 1 * |(x ^ 2)| := by simpa
64 simpa using this
65
66/-- O(f) + O(g) = O(h). -/