bigO_add

formal source

  64  simpa using this
  65
  66/-- O(f) + O(g) = O(h). -/
  67theorem bigO_add (f g h : ℝ → ℝ) (a : ℝ) :
  68  IsBigO f h a → IsBigO g h a → IsBigO (fun x => f x + g x) h a := by
  69  intro hf hg
  70  rcases hf with ⟨C₁, hC₁pos, M₁, hM₁pos, hf⟩
  71  rcases hg with ⟨C₂, hC₂pos, M₂, hM₂pos, hg⟩
  72  have hMinPos : 0 < min M₁ M₂ := lt_min hM₁pos hM₂pos
  73  refine ⟨C₁ + C₂, by linarith, min M₁ M₂, hMinPos, ?_⟩
  74  intro x hx
  75  have hx₁ : |x - a| < M₁ := lt_of_lt_of_le hx (min_le_left _ _)
  76  have hx₂ : |x - a| < M₂ := lt_of_lt_of_le hx (min_le_right _ _)
  77  have hf' := hf x hx₁
  78  have hg' := hg x hx₂
  79  have htri : |f x + g x| ≤ |f x| + |g x| := abs_add_le _ _
  80  have hsum : |f x| + |g x| ≤ (C₁ + C₂) * |h x| := by
  81    have hadd := add_le_add hf' hg'
  82    linarith [mul_nonneg (le_of_lt hC₁pos) (abs_nonneg (h x)),
  83              mul_nonneg (le_of_lt hC₂pos) (abs_nonneg (h x))]
  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 _ _)