linear_is_O_x
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not claim the bound holds for |x| >= M.
- Does not optimize C for specific c or yield little-o statements.
- Does not extend to limits at infinity or other base points.
- Does not assume extra regularity such as differentiability.
formal statement (Lean)
45theorem linear_is_O_x (c : ℝ) :
46 IsBigO (fun x => c * x) (fun x => x) 0 := by
proof body
Tactic-mode proof.
47 unfold IsBigO
48 have hpos : (0 : ℝ) < |c| + 1 := by have := abs_nonneg c; linarith
49 refine ⟨|c| + 1, hpos, 1, by norm_num, ?_⟩
50 intro x _
51 rw [abs_mul]
52 have h1 : |c| ≤ |c| + 1 := by linarith
53 have h2 : |c| * |x| ≤ (|c| + 1) * |x| := by
54 apply mul_le_mul_of_nonneg_right h1 (abs_nonneg _)
55 exact h2
56
57/-- x² is O(x²) (reflexive). -/