bigO_const_mul
This theorem shows that scalar multiplication by any real constant preserves the big-O relation: if f is big-O of g near a, then c times f is also big-O of g near a. Analysts using asymptotic estimates in relativity models or recognition-based derivations would invoke it to scale bounds without changing the reference function. The proof constructs an explicit new witness constant (|c| + 1) times the original C and verifies the inequality via absolute-value identities and linear arithmetic.
claimIf $f = O(g)$ as $x$ approaches $a$, then the scaled function $xmapsto c f(x)$ satisfies $c f = O(g)$ as $x$ approaches $a$, for any real scalar $c$.
background
The module supplies a rigorous Filter-based definition of Landau big-O notation for real functions. IsBigO(f, g, a) holds when there exist C > 0 and M > 0 such that |x - a| < M implies |f(x)| ≤ C |g(x)|. The local setting is arithmetic closure of asymptotic classes under addition, multiplication, and scalar scaling, needed for manipulating estimates that arise from the Recognition Composition Law (the d'Alembert equation F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y) for positive arguments). Upstream results supply the base IsBigO predicate and the Composition axiom that forces multiplicative consistency in the underlying recognition structure.
proof idea
The tactic proof introduces the hypothesis, destructures the existential witnesses C, M and their positivity proofs, then builds a new positive constant (|c| + 1) C. It refines the existential and, inside the universal quantifier, rewrites |c f(x)| via abs_mul, applies mul_le_mul_of_nonneg_left to the original bound, and closes the final inequality with nlinarith using non-negativity of absolute values.
why it matters in Recognition Science
The result supplies one of the elementary arithmetic operations required to keep asymptotic classes closed under the operations that appear when deriving limits from the Recognition Composition Law and the eight-tick octave structure. It sits inside the Landau-analysis layer that supports later relativity estimates; although no direct downstream use is recorded yet, the lemma closes a basic manipulation gap that would otherwise force repeated manual constant adjustments in any chain relying on scaled forcing terms.
scope and limits
- Does not prove the converse implication.
- Does not treat the little-o case.
- Does not extend to functions taking values in normed spaces.
- Does not supply explicit optimal constants for concrete f and g.
formal statement (Lean)
71theorem bigO_const_mul (c : ℝ) (f g : ℝ → ℝ) (a : ℝ) :
72 IsBigO f g a → IsBigO (fun x => c * f x) g a := by
proof body
Tactic-mode proof.
73 intro hf
74 rcases hf with ⟨C, hCpos, M, hMpos, hbound⟩
75 have hCpos' : 0 < (|c| + 1) * C := by
76 have h1 : 0 < |c| + 1 := by have := abs_nonneg c; linarith
77 exact mul_pos h1 hCpos
78 refine ⟨(|c| + 1) * C, hCpos', M, hMpos, ?_⟩
79 intro x hx
80 have hx' := hbound x hx
81 calc |c * f x|
82 = |c| * |f x| := abs_mul _ _
83 _ ≤ |c| * (C * |g x|) := mul_le_mul_of_nonneg_left hx' (abs_nonneg c)
84 _ ≤ (|c| + 1) * C * |g x| := by nlinarith [abs_nonneg c, abs_nonneg (g x)]
85
86/-- Composition with continuous function (placeholder: keep axiomatized for now). -/