bigO_comp
The theorem proves that if f is asymptotically bounded by g near a, h is pointwise dominated by g, and k is uniformly bounded, then the product k composed with f times h remains asymptotically bounded by g near a. Analysts in mathematical physics would cite this when composing error terms in limit analyses. The proof works by extracting the bound constant for k, unfolding the big-O definition, and chaining multiplication inequalities on absolute values.
claimSuppose $f, g, h, k : ℝ → ℝ$ and $a ∈ ℝ$. Assume $f = O(g)$ as $x → a$, there exists $K > 0$ such that $|k(y)| ≤ K$ for all $y$, and $|h(x)| ≤ |g(x)|$ for all $x$. Then $k(f(x)) · h(x) = O(g)$ as $x → a$.
background
The module integrates Mathlib asymptotics to replace placeholder error bounds with explicit notation. The central definition states that f is big-O of g near a when there exist C > 0 and M > 0 such that |x - a| < M implies |f x| ≤ C |g x|.
proof idea
The proof rcases the existential bound on k to obtain positive K. It unfolds the big-O predicate, refines witnesses C = K and M = 1, then applies abs_mul followed by a calc chain using mul_le_mul_of_nonneg_right and mul_le_mul_of_nonneg_left to close the inequality.
why it matters in Recognition Science
This supplies a basic composition rule for big-O notation in the relativity limits module. It supports rigorous asymptotic control needed for deriving constants such as the bridge ratio K = phi^{1/2} and spatial dimension D = 3. No downstream theorems depend on it yet, leaving it available for chaining error estimates in physical derivations.
scope and limits
- Does not address the general case where k must approach zero.
- Does not incorporate filter-based Mathlib asymptotics.
- Does not extend to little-o or vector-valued functions.
- Does not apply outside real-valued functions on the line.
formal statement (Lean)
110theorem bigO_comp (f g h : ℝ → ℝ) (k : ℝ → ℝ) (a : ℝ)
111 (hfg : IsBigO f g a)
112 (hk_bound : ∃ K > 0, ∀ y, |k y| ≤ K) -- Simplified: k uniformly bounded
113 (hg : ∀ x, |h x| ≤ |g x|) :
114 IsBigO (fun x => k (f x) * h x) (fun x => g x) a := by
proof body
Tactic-mode proof.
115 -- With k uniformly bounded by K, we have |k(f x) * h x| ≤ K * |h x| ≤ K * |g x|
116 rcases hk_bound with ⟨K, hKpos, hK⟩
117 unfold IsBigO
118 refine ⟨K, hKpos, 1, by norm_num, ?_⟩
119 intro x _
120 rw [abs_mul]
121 have hk_fx : |k (f x)| ≤ K := hK (f x)
122 have hh_x : |h x| ≤ |g x| := hg x
123 calc |k (f x)| * |h x| ≤ K * |h x| := by
124 apply mul_le_mul_of_nonneg_right hk_fx (abs_nonneg _)
125 _ ≤ K * |g x| := by
126 apply mul_le_mul_of_nonneg_left hh_x (le_of_lt hKpos)
127
128/-- Little-o is stronger than big-O. -/