bigO_mul_subset
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not address little-o notation or other Landau symbols.
- Does not treat functions taking values in normed spaces beyond reals.
- Does not supply explicit constants for concrete choices of f and g.
- Does not extend the neighborhood to include the point a itself.
formal statement (Lean)
51theorem bigO_mul_subset (f g : ℝ → ℝ) (a : ℝ) :
52 ∀ h₁ h₂, IsBigO h₁ f a → IsBigO h₂ g a →
53 IsBigO (fun x => h₁ x * h₂ x) (fun x => f x * g x) a := by
proof body
Tactic-mode proof.
54 intro h₁ h₂ hf hg
55 rcases hf with ⟨C₁, hC₁pos, M₁, hM₁pos, hf⟩
56 rcases hg with ⟨C₂, hC₂pos, M₂, hM₂pos, hg⟩
57 refine ⟨C₁ * C₂, by nlinarith, min M₁ M₂, lt_min hM₁pos hM₂pos, ?_⟩
58 intro x hx
59 have hx₁ : |x - a| < M₁ := lt_of_lt_of_le hx (min_le_left _ _)
60 have hx₂ : |x - a| < M₂ := lt_of_lt_of_le hx (min_le_right _ _)
61 have hf' := hf x hx₁
62 have hg' := hg x hx₂
63 calc |h₁ x * h₂ x|
64 = |h₁ x| * |h₂ x| := abs_mul _ _
65 _ ≤ (C₁ * |f x|) * (C₂ * |g x|) :=
66 mul_le_mul hf' hg' (abs_nonneg _) (by linarith [mul_nonneg (le_of_lt hC₁pos) (abs_nonneg (f x))])
67 _ = (C₁ * C₂) * (|f x| * |g x|) := by ring
68 _ = (C₁ * C₂) * |f x * g x| := by rw [abs_mul]
69
70/-- Scalar multiplication: c · O(f) = O(g) when f = O(g). -/