const_is_O_one
plain-language theorem explainer
Constant real functions satisfy big-O of the unit constant at the origin. Analysts replacing placeholder error bounds in relativistic asymptotic expansions cite this when controlling trivial terms. The tactic proof unfolds the existential definition of IsBigO, exhibits explicit C = |c| + 1 and M = 1, then closes the inequality with linear arithmetic and simplification.
Claim. For every real number $c$, the constant function $f(x) = c$ satisfies $f = O(1)$ at $0$: there exist $C > 0$ and $M > 0$ such that $|x| < M$ implies $|c| ≤ C · 1$.
background
The module integrates Mathlib asymptotics to supply rigorous big-O and little-o notation, replacing placeholder error bounds with Filter-based definitions. IsBigO(f, g, a) asserts existence of C > 0 and M > 0 such that |x - a| < M implies |f(x)| ≤ C |g(x)|. This supplies the basic constant case needed before composing bounds via the sibling lemmas bigO_add and bigO_mul.
proof idea
Unfolds IsBigO to expose the quantifiers. Constructs C = |c| + 1 (positive by abs_nonneg and linarith) and M = 1. For |x| < 1 the inequality |c| ≤ |c| + 1 holds by linarith; simp reduces |1| and applies mul_one to finish the bound.
why it matters
Supplies the trivial constant bound that anchors the asymptotic toolkit in the relativity analysis module. It precedes the composition and transitivity lemmas (bigO_add, bigO_mul, littleO_bigO_trans) that control error terms arising from the forcing chain and phi-ladder constructions. No downstream uses are recorded, indicating it functions as a local primitive rather than a cross-module interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.