theorem
proved
tactic proof
bigO_mul
show as:
view Lean formalization →
formal statement (Lean)
87theorem bigO_mul (f₁ f₂ g₁ g₂ : ℝ → ℝ) (a : ℝ) :
88 IsBigO f₁ g₁ a → IsBigO f₂ g₂ a → IsBigO (fun x => f₁ x * f₂ x) (fun x => g₁ x * g₂ x) a := by
proof body
Tactic-mode proof.
89 intro hf hg
90 rcases hf with ⟨C₁, hC₁pos, M₁, hM₁pos, hf⟩
91 rcases hg with ⟨C₂, hC₂pos, M₂, hM₂pos, hg⟩
92 have hMinPos : 0 < min M₁ M₂ := lt_min hM₁pos hM₂pos
93 have hCpos : 0 < C₁ * C₂ := mul_pos hC₁pos hC₂pos
94 refine ⟨C₁ * C₂, hCpos, min M₁ M₂, hMinPos, ?_⟩
95 intro x hx
96 have hx₁ : |x - a| < M₁ := lt_of_lt_of_le hx (min_le_left _ _)
97 have hx₂ : |x - a| < M₂ := lt_of_lt_of_le hx (min_le_right _ _)
98 have hf' := hf x hx₁
99 have hg' := hg x hx₂
100 rw [abs_mul, abs_mul]
101 have hmul := mul_le_mul hf' hg' (abs_nonneg _) (by linarith [mul_nonneg (le_of_lt hC₁pos) (abs_nonneg (g₁ x))])
102 calc |f₁ x| * |f₂ x| ≤ (C₁ * |g₁ x|) * (C₂ * |g₂ x|) := hmul
103 _ = (C₁ * C₂) * (|g₁ x| * |g₂ x|) := by ring
104
105/-- Composition preserves O(·) when k is uniformly bounded.
106
107 This simplified version assumes k is uniformly bounded, which is
108 sufficient for our applications. The more general version would require
109 k → 0 as its argument → 0, combined with f → 0 as x → a. -/