Squeeze Theorem

The squeeze theorem (also called the sandwich or pinching theorem) is the workhorse for evaluating limits that resist direct computation. If two sequences converge to the same value and a third sequence is forever trapped between them, there is nowhere else for it to go.

Statement

Let $a_n$, $b_n$, $c_n$ be real sequences. Suppose

and

Then $b_n$ converges and $\lim_{n \to \infty} b_n = L$.

The same statement holds for real-valued functions on a metric space, and more generally for any sequence valued in a topological ordered space.

Visualization

The classic example is $b_n = \sin(n)/n$, squeezed between $a_n = -1/n$ and $c_n = 1/n$.

 n   |  a_n = -1/n  |  b_n = sin(n)/n  |  c_n = 1/n
-----|--------------|------------------|------------
  1  |  -1.000      |   0.841          |  1.000
  2  |  -0.500      |   0.455          |  0.500
  5  |  -0.200      |  -0.192          |  0.200
 10  |  -0.100      |  -0.054          |  0.100
 20  |  -0.050      |   0.046          |  0.050
 50  |  -0.020      |  -0.019          |  0.020
100  |  -0.010      |  -0.005          |  0.010

Both outer sequences tend to $0$, so $b_n \to 0$ even though $\sin(n)$ itself never settles.

A schematic view of the three curves converging:

 1/n  ···──────────────────────────────► 0
       \      sin(n)/n (oscillates)
-1/n  ···──────────────────────────────► 0

Proof Sketch

Fix $\varepsilon > 0$. Since $a_n \to L$ there exists $N_1$ such that $|a_n - L| < \varepsilon$ for $n \geq N_1$, and since $c_n \to L$ there exists $N_2$ such that $|c_n - L| < \varepsilon$ for $n \geq N_2$. For $n \geq \max(N_1, N_2)$:

so $|b_n - L| < \varepsilon$.

Connections

The squeeze theorem is the standard route to limits like $\lim_{x\to 0} x \sin(1/x) = 0$, and it underpins the proof of Intermediate Value TheoremIntermediate Value Theorem$$f(a) \le y \le f(b) \Rightarrow \exists\, c \in [a,b]:\; f(c) = y$$A continuous function on a closed interval hits every value between its endpointsRead more → (via the nested-interval argument). In the continuous setting it combines with the Mean Value TheoremMean Value Theorem$$\exists\, c \in (a,b)\;:\; f'(c) = \frac{f(b)-f(a)}{b-a}$$There exists a point where the instantaneous rate of change equals the average rate of changeRead more → to bound derivative estimates. The bounded-oscillation intuition resurfaces in Cauchy CriterionCauchy Criterion$$\forall\varepsilon>0\;\exists N:\; m,n \geq N \implies |a_m - a_n| < \varepsilon$$A sequence converges if and only if its terms eventually become arbitrarily close to each other — no candidate limit requiredRead more → (a sequence that satisfies the Cauchy condition is itself squeezed between its own partial sup/inf). Within this section see also Monotone Convergence TheoremMonotone Convergence Theorem$$f \text{ monotone},\; \sup_n f(n) < \infty \implies f(n) \to \sup_n f(n)$$A bounded monotone sequence of reals always converges — the supremum is the limitRead more → for the case where $b_n$ is forced to converge by monotonicity rather than by a bounding pair.

import Mathlib.Topology.Order.Basic

open Filter Topology

/-- Squeeze theorem for sequences: a sequence sandwiched between two sequences
    with a common limit must share that limit. -/
theorem squeeze {a b c : ℕ → ℝ} {L : ℝ}
    (ha : Tendsto a atTop (𝓝 L))
    (hc : Tendsto c atTop (𝓝 L))
    (hab : ∀ n, a n ≤ b n)
    (hbc : ∀ n, b n ≤ c n) :
    Tendsto b atTop (𝓝 L) :=
  tendsto_of_tendsto_of_tendsto_of_le_of_le ha hc
    (fun n => hab n) (fun n => hbc n)