bigO_add
plain-language theorem explainer
If f and g are each big-O of h near a, then their sum is also big-O of h near a. Analysts merging asymptotic error terms in relativity models cite this to combine separate bounds. The tactic proof unpacks the four witnesses from each hypothesis, forms the summed constant and minimum radius, then chains the triangle inequality through order transitivity.
Claim. If there exist $C_1 > 0$, $M_1 > 0$ such that $|f(x)| ≤ C_1 |h(x)|$ for all $x$ with $|x-a| < M_1$, and likewise $C_2 > 0$, $M_2 > 0$ for $g$, then there exist $C > 0$, $M > 0$ such that $|f(x) + g(x)| ≤ C |h(x)|$ whenever $|x-a| < M$.
background
The module supplies rigorous big-O and little-o notation for relativity analysis by importing Mathlib asymptotics and replacing informal bounds. IsBigO(f, h, a) is the predicate asserting existence of positive C and M such that |f(x)| ≤ C |h(x)| holds for |x-a| < M; this definition is the only local hypothesis type appearing in the signature.
proof idea
The tactic proof introduces the two hypotheses and rcases each into its witnesses C, M and inequality. It constructs the summed constant and minimum radius as new witnesses, then for x inside the minimum radius retrieves the separate bounds, applies the triangle inequality to |f+g|, adds the scaled terms, and closes with le_trans.
why it matters
The declaration supplies a basic closure property under addition for the O-notation used throughout the relativity module. It enables merging of independent error estimates without leaving the big-O class. No downstream applications are recorded, yet the result fills a standard algebraic requirement for any complete asymptotic system.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.