bigO_mul

formal source

  84  exact le_trans htri hsum
  85
  86/-- O(f) · O(g) = O(f·g). -/
  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
  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. -/
 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