bigO_mul_subset
plain-language theorem explainer
The theorem shows that the product of two big-O functions remains big-O of the product of their targets near the same point a. Analysts composing asymptotic bounds in relativity models would cite it when multiplying error estimates. The proof extracts witnessing constants and radii from each hypothesis then combines them via absolute-value identities and monotonicity of multiplication.
Claim. If $h_1 = O(f)$ and $h_2 = O(g)$ near $a$, then $h_1 h_2 = O(f g)$ near $a$.
background
The module supplies rigorous Landau big-O notation for real-valued functions of one real variable. IsBigO f g a asserts the existence of C > 0 and M > 0 such that |f(x)| ≤ C |g(x)| whenever |x - a| < M. This definition is imported from the Limits module and is used to equip the big-O classes with arithmetic operations.
proof idea
The tactic proof introduces the two hypotheses, performs rcases to obtain the four witnesses C1, M1, C2, M2, then refines to the product constant C1 C2 and the minimum radius. Inside the goal it splits the neighborhood conditions, applies the original bounds, and chains abs_mul, mul_le_mul, ring, and abs_mul again to close the inequality.
why it matters
The result supplies the multiplicative closure property for big-O classes inside the Landau notation layer of the relativity analysis module. It directly supports the arithmetic manipulation lemmas listed as siblings and is required for any later composition of asymptotic expressions in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.