bigO_add
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.
claimIf 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 in Recognition Science
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.
scope and limits
- Does not compute explicit numerical values for C or M.
- Does not treat little-o or other asymptotic relations.
- Does not assume continuity or differentiability of any function.
- Does not cover the case where h vanishes identically near a.
formal statement (Lean)
67theorem bigO_add (f g h : ℝ → ℝ) (a : ℝ) :
68 IsBigO f h a → IsBigO g h a → IsBigO (fun x => f x + g x) h a := by
proof body
Tactic-mode proof.
69 intro hf hg
70 rcases hf with ⟨C₁, hC₁pos, M₁, hM₁pos, hf⟩
71 rcases hg with ⟨C₂, hC₂pos, M₂, hM₂pos, hg⟩
72 have hMinPos : 0 < min M₁ M₂ := lt_min hM₁pos hM₂pos
73 refine ⟨C₁ + C₂, by linarith, min M₁ M₂, hMinPos, ?_⟩
74 intro x hx
75 have hx₁ : |x - a| < M₁ := lt_of_lt_of_le hx (min_le_left _ _)
76 have hx₂ : |x - a| < M₂ := lt_of_lt_of_le hx (min_le_right _ _)
77 have hf' := hf x hx₁
78 have hg' := hg x hx₂
79 have htri : |f x + g x| ≤ |f x| + |g x| := abs_add_le _ _
80 have hsum : |f x| + |g x| ≤ (C₁ + C₂) * |h x| := by
81 have hadd := add_le_add hf' hg'
82 linarith [mul_nonneg (le_of_lt hC₁pos) (abs_nonneg (h x)),
83 mul_nonneg (le_of_lt hC₂pos) (abs_nonneg (h x))]
84 exact le_trans htri hsum
85
86/-- O(f) · O(g) = O(f·g). -/