linear_is_O_x

formal source

  42  exact h1
  43
  44/-- Linear function is O(x). -/
  45theorem linear_is_O_x (c : ℝ) :
  46  IsBigO (fun x => c * x) (fun x => x) 0 := by
  47  unfold IsBigO
  48  have hpos : (0 : ℝ) < |c| + 1 := by have := abs_nonneg c; linarith
  49  refine ⟨|c| + 1, hpos, 1, by norm_num, ?_⟩
  50  intro x _
  51  rw [abs_mul]
  52  have h1 : |c| ≤ |c| + 1 := by linarith
  53  have h2 : |c| * |x| ≤ (|c| + 1) * |x| := by
  54    apply mul_le_mul_of_nonneg_right h1 (abs_nonneg _)
  55  exact h2
  56
  57/-- x² is O(x²) (reflexive). -/
  58theorem x_squared_is_O_x_squared :
  59  IsBigOPower (fun x => x ^ 2) 2 := by
  60  unfold IsBigOPower IsBigO
  61  refine ⟨1, by norm_num, 1, by norm_num, ?_⟩
  62  intro x _
  63  have : |(x ^ 2)| ≤ 1 * |(x ^ 2)| := by simpa
  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 _ _)