theorem
proved
tactic proof
bigO_comp
show as:
view Lean formalization →
formal statement (Lean)
110theorem bigO_comp (f g h : ℝ → ℝ) (k : ℝ → ℝ) (a : ℝ)
111 (hfg : IsBigO f g a)
112 (hk_bound : ∃ K > 0, ∀ y, |k y| ≤ K) -- Simplified: k uniformly bounded
113 (hg : ∀ x, |h x| ≤ |g x|) :
114 IsBigO (fun x => k (f x) * h x) (fun x => g x) a := by
proof body
Tactic-mode proof.
115 -- With k uniformly bounded by K, we have |k(f x) * h x| ≤ K * |h x| ≤ K * |g x|
116 rcases hk_bound with ⟨K, hKpos, hK⟩
117 unfold IsBigO
118 refine ⟨K, hKpos, 1, by norm_num, ?_⟩
119 intro x _
120 rw [abs_mul]
121 have hk_fx : |k (f x)| ≤ K := hK (f x)
122 have hh_x : |h x| ≤ |g x| := hg x
123 calc |k (f x)| * |h x| ≤ K * |h x| := by
124 apply mul_le_mul_of_nonneg_right hk_fx (abs_nonneg _)
125 _ ≤ K * |g x| := by
126 apply mul_le_mul_of_nonneg_left hh_x (le_of_lt hKpos)
127
128/-- Little-o is stronger than big-O. -/