const_is_O_one
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish little-o behavior for constants.
- Does not address limits at infinity or other filters.
- Does not extend to vector-valued or complex-valued functions.
- Does not supply explicit decay rates beyond existence of C and M.
formal statement (Lean)
34theorem const_is_O_one (c : ℝ) :
35 IsBigO (fun _ => c) (fun _ => 1) 0 := by
proof body
Tactic-mode proof.
36 unfold IsBigO
37 have hpos : (0 : ℝ) < |c| + 1 := by have := abs_nonneg c; linarith
38 refine ⟨|c| + 1, hpos, 1, by norm_num, ?_⟩
39 intro x _
40 have h1 : |c| ≤ |c| + 1 := by linarith
41 simp only [abs_one, mul_one]
42 exact h1
43
44/-- Linear function is O(x). -/