theorem
proved
tactic proof
bigO_add_subset
show as:
view Lean formalization →
formal statement (Lean)
24theorem bigO_add_subset (f g : ℝ → ℝ) (a : ℝ) :
25 ∀ h₁ h₂, IsBigO h₁ f a → IsBigO h₂ g a →
26 IsBigO (fun x => h₁ x + h₂ x) (fun x => max (|f x|) (|g x|)) a := by
proof body
Tactic-mode proof.
27 intro h₁ h₂ hf hg
28 rcases hf with ⟨C₁, hC₁pos, M₁, hM₁pos, hf⟩
29 rcases hg with ⟨C₂, hC₂pos, M₂, hM₂pos, hg⟩
30 refine ⟨C₁ + C₂, by linarith, min M₁ M₂, lt_min hM₁pos hM₂pos, ?_⟩
31 intro x hx
32 have hx₁ : |x - a| < M₁ := lt_of_lt_of_le hx (min_le_left _ _)
33 have hx₂ : |x - a| < M₂ := lt_of_lt_of_le hx (min_le_right _ _)
34 have hf' := hf x hx₁
35 have hg' := hg x hx₂
36 -- Triangle inequality and bounds
37 have hmax_nonneg : 0 ≤ max (|f x|) (|g x|) := le_max_of_le_left (abs_nonneg _)
38 calc |h₁ x + h₂ x|
39 ≤ |h₁ x| + |h₂ x| := abs_add_le _ _
40 _ ≤ C₁ * |f x| + C₂ * |g x| := add_le_add hf' hg'
41 _ ≤ C₁ * max (|f x|) (|g x|) + C₂ * max (|f x|) (|g x|) := by
42 have h1 : C₁ * |f x| ≤ C₁ * max (|f x|) (|g x|) :=
43 mul_le_mul_of_nonneg_left (le_max_left _ _) (le_of_lt hC₁pos)
44 have h2 : C₂ * |g x| ≤ C₂ * max (|f x|) (|g x|) :=
45 mul_le_mul_of_nonneg_left (le_max_right _ _) (le_of_lt hC₂pos)
46 exact add_le_add h1 h2
47 _ = (C₁ + C₂) * max (|f x|) (|g x|) := by ring
48 _ = (C₁ + C₂) * |max (|f x|) (|g x|)| := by rw [abs_of_nonneg hmax_nonneg]
49
50/-- O(f) · O(g) ⊆ O(f·g). -/