bigO_comp

formal source

 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. -/
 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
 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. -/
 129theorem littleO_implies_bigO (f g : ℝ → ℝ) (a : ℝ) :
 130  IsLittleO f g a → IsBigO f g a := by
 131  intro h
 132  -- Use ε = 1 to obtain a specific bound
 133  have hε := h 1 (by norm_num : (0 : ℝ) < 1)
 134  rcases hε with ⟨M, hMpos, hbound⟩
 135  refine ⟨1, by norm_num, M, hMpos, ?_⟩
 136  intro x hx
 137  simpa using hbound x hx
 138
 139/-- f = o(g) and g = O(h) implies f = o(h). -/
 140theorem littleO_bigO_trans (f g h : ℝ → ℝ) (a : ℝ) :