bigO_comp
plain-language theorem explainer
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.
Claim. Suppose $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.