x_squared_is_O_x_squared
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.