bigO_mul
plain-language theorem explainer
The theorem shows that the product of two functions each big-O of their respective bounds near a remains big-O of the product bound. Analysts deriving multiplicative error estimates in recognition models cite it when combining asymptotic terms. The proof extracts witnessing constants and radii from each hypothesis, forms their product and minimum, then verifies the combined inequality with absolute-value multiplication and monotonicity.
Claim. If $f_1 = O(g_1)$ and $f_2 = O(g_2)$ at $a$, then $f_1 f_2 = O(g_1 g_2)$ at $a$, where $f = O(g)$ at $a$ means there exist $C > 0$, $M > 0$ such that $|f(x)| ≤ C |g(x)|$ for all $|x - a| < M$.
background
The module supplies rigorous big-O and little-o notation by integrating Mathlib asymptotics, replacing placeholder error bounds with Filter-based definitions. IsBigO(f, g, a) is the predicate asserting existence of positive C and M such that |f(x)| ≤ C |g(x)| whenever |x - a| < M. The local setting is asymptotic analysis for limits in the recognition framework.
proof idea
Tactic proof: introduce the two hypotheses, rcases each to obtain C1, M1 and C2, M2. Form the combined witness C1*C2 (positive by mul_pos) and radius min(M1, M2) (positive by lt_min). For x inside the min radius, apply the individual bounds, rewrite with abs_mul, invoke mul_le_mul on the absolute values, then simplify the right-hand side by ring.
why it matters
It supplies the multiplicative closure property needed for composing asymptotic estimates inside the relativity analysis module. The result supports error-bound manipulation that appears in forcing-chain steps T5-T8 and in applications of the Recognition Composition Law. No downstream uses are recorded, leaving it as a foundational tool for later limit arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.