def Sequences.RealSequence : Type

A real sequence is a function from the natural numbers to the reals, i.e. ℕ → ℝ.

def Sequences.IsBoundedSeq (x : ℕ → ℝ) : Prop

A real sequence x is bounded if there exists a non-negative real B such that |x n| ≤ B for every n : ℕ.

theorem Sequences.seq_converges_iff (x : ℕ → ℝ) (L : ℝ) : Filter.Tendsto x Filter.atTop (nhds L) ↔ ∀ ε > 0, ∃ (M : ℕ), ∀ n ≥ M, |x n - L| < ε

ε–N characterization of convergence: x n → L if and only if for every ε > 0 there exists M : ℕ such that |x n - L| < ε for all n ≥ M.

theorem Sequences.squeeze_theorem (a x b : ℕ → ℝ) (L : ℝ) (hab : ∀ (n : ℕ), a n ≤ x n) (hxb : ∀ (n : ℕ), x n ≤ b n) (ha : Filter.Tendsto a Filter.atTop (nhds L)) (hb : Filter.Tendsto b Filter.atTop (nhds L)) : Filter.Tendsto x Filter.atTop (nhds L)

Squeeze (sandwich) theorem for real sequences: if a n ≤ x n ≤ b n for all n and both a and b converge to the same limit L, then x also converges to L.