IsLittleO

formal source

  19  ∃ C > 0, ∃ M > 0, ∀ x, |x - a| < M → |f x| ≤ C * |g x|
  20
  21/-- Little-o notation: ∀ ε > 0, ∃ M such that |f(x)| ≤ ε|g(x)| for |x-a| < M. -/
  22def IsLittleO (f g : ℝ → ℝ) (a : ℝ) : Prop :=
  23  ∀ ε > 0, ∃ M > 0, ∀ x, |x - a| < M → |f x| ≤ ε * |g x|
  24
  25/-- f = O(x^n) as x → 0. -/
  26def IsBigOPower (f : ℝ → ℝ) (n : ℕ) : Prop :=
  27  IsBigO f (fun x => x ^ n) 0
  28
  29/-- f = o(x^n) as x → 0. -/
  30def IsLittleOPower (f : ℝ → ℝ) (n : ℕ) : Prop :=
  31  IsLittleO f (fun x => x ^ n) 0
  32
  33/-- Constant function is O(1). -/
  34theorem const_is_O_one (c : ℝ) :
  35  IsBigO (fun _ => c) (fun _ => 1) 0 := by
  36  unfold IsBigO
  37  have hpos : (0 : ℝ) < |c| + 1 := by have := abs_nonneg c; linarith
  38  refine ⟨|c| + 1, hpos, 1, by norm_num, ?_⟩
  39  intro x _
  40  have h1 : |c| ≤ |c| + 1 := by linarith
  41  simp only [abs_one, mul_one]
  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