2.1. First examples🔗

Given two sequences of real numbers, a_n and b_n, Mathlib allows one to say that a = O(b) by writing simply a =O[atTop] b. We can witness that this means what we expect as follows:

example (a b : ℕ → ℝ) :
    a =O[atTop] b ↔
      ∃ C N, ∀ n ≥ N, ‖a n‖ ≤ C * ‖b n‖ := bya:ℕ → ℝb:ℕ → ℝ⊢ a =O[atTop] b ↔ ∃ C N, ∀ n ≥ N, ‖a n‖ ≤ C * ‖b n‖
  simp_rw [a:ℕ → ℝb:ℕ → ℝ⊢ a =O[atTop] b ↔ ∃ C N, ∀ n ≥ N, ‖a n‖ ≤ C * ‖b n‖isBigO_iff,a:ℕ → ℝb:ℕ → ℝ⊢ (∃ c, ∀ᶠ (x : ℕ) in atTop, ‖a x‖ ≤ c * ‖b x‖) ↔ ∃ C N, ∀ n ≥ N, ‖a n‖ ≤ C * ‖b n‖ eventually_atTopAll goals completed! 🐙]

If instead we have functions f, g : ℝ → ℝ, the same notation works:

example (f g : ℝ → ℝ) :
    f =O[atTop] g ↔
      ∃ C N, ∀ n ≥ N, ‖f n‖ ≤ C * ‖g n‖ := byf:ℝ → ℝg:ℝ → ℝ⊢ f =O[atTop] g ↔ ∃ C N, ∀ n ≥ N, ‖f n‖ ≤ C * ‖g n‖
  simp_rw [f:ℝ → ℝg:ℝ → ℝ⊢ f =O[atTop] g ↔ ∃ C N, ∀ n ≥ N, ‖f n‖ ≤ C * ‖g n‖isBigO_iff,f:ℝ → ℝg:ℝ → ℝ⊢ (∃ c, ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c * ‖g x‖) ↔ ∃ C N, ∀ n ≥ N, ‖f n‖ ≤ C * ‖g n‖ eventually_atTopAll goals completed! 🐙]