bigO_add_subset
plain-language theorem explainer
The theorem asserts that the sum of two functions each asymptotically dominated by f and g near a point a is itself dominated by the pointwise maximum of their absolute values. Analysts combining error estimates in asymptotic expansions for relativistic models would cite this closure property. The argument extracts the witnessing constants and radii from each Big-O hypothesis, assembles their sum and minimum, and closes via the triangle inequality together with monotonicity of the max function.
Claim. If there exist positive constants $C_1,M_1$ such that $|h_1(x)|$ is at most $C_1|f(x)|$ for all $x$ with $|x-a|<M_1$, and positive constants $C_2,M_2$ such that $|h_2(x)|$ is at most $C_2|g(x)|$ for all $x$ with $|x-a|<M_2$, then there exist positive constants $C,M$ such that $|h_1(x)+h_2(x)|$ is at most $C$ times the maximum of $|f(x)|$ and $|g(x)|$ whenever $|x-a|<M$.
background
The module supplies a rigorous implementation of Landau notation in which $k$ belongs to $O(m)$ at $a$ precisely when positive constants $C$ and $M$ exist satisfying $|k(x)|$ at most $C|m(x)|$ for every $x$ with $|x-a|<M$. This explicit existential form supports direct algebraic manipulation of asymptotic classes, including the addition and multiplication operations treated by the sibling lemmas in the same file. The IsBigO predicate is defined exactly by the witness statement above; the imported Triangle structure and log-derivative bound play no role in the present argument.
proof idea
The tactic proof introduces the two functions and their Big-O assumptions, then destructures each assumption to obtain the four witnesses $C_1,M_1,C_2,M_2$. A single combined witness is assembled with constant $C_1+C_2$ and radius the minimum of $M_1$ and $M_2$. Inside this common neighborhood the triangle inequality bounds the absolute value of the sum by the sum of the absolute values; each term is replaced by its Big-O estimate and the resulting expression is majorized by the combined constant times the maximum via the two inequalities $C_i$ times the absolute value is at most $C_i$ times the max.
why it matters
The lemma supplies a basic closure property under addition for the Big-O relation and belongs to the collection of Landau arithmetic facts that enable systematic manipulation of asymptotic error terms inside the relativity analysis module. It complements the sibling results on multiplication, constant multiples, and composition. No immediate parent theorems are recorded among the dependents, yet the result is required for any consistent calculus of Big-O classes that would later support error-term bookkeeping in derivations of the spatial dimension or the fine-structure constant band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.