linear_is_O_x
plain-language theorem explainer
Any linear function x |-> c x is big-O of x near zero. Analysts bounding linear perturbations in relativistic expansions cite this to justify first-order error controls. The tactic proof unfolds IsBigO, supplies the explicit witnesses C = |c| + 1 and M = 1, then verifies the inequality via absolute-value rewriting and monotonicity of multiplication.
Claim. For every real $c$, the map $xmapsto c x$ satisfies the big-O relation with respect to $xmapsto x$ at $0$: there exist $C>0$ and $M>0$ such that $|c x|leq C|x|$ for all $x$ with $|x|<M$.
background
The module integrates Mathlib asymptotics to replace placeholder error bounds with Filter-based definitions. IsBigO(f,g,a) means there exist C>0 and M>0 such that |f(x)|leq C|g(x)| whenever |x-a|<M. The local setting is asymptotic analysis for relativity models, where linear terms appear in expansions around the origin.
proof idea
The tactic proof unfolds IsBigO, constructs the witness C = |c| + 1 (positive by abs_nonneg and linarith) together with M = 1, then enters the forall. It rewrites abs_mul, bounds |c| by |c| + 1, multiplies the inequality by the nonnegative |x|, and closes with exact.
why it matters
The declaration supplies a basic linear instance inside the Limits submodule, enabling rigorous control of first-order terms in relativistic analysis. It supports replacement of informal bounds by the module's O notation without touching the forcing chain or phi-ladder. No downstream uses are recorded, so its role remains local to error estimates near zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.