Epsilon-Delta Proof

Prove limit statements using the rigorous epsilon-delta definition.

The Definition

For a limit: lim_{x→a} f(x) = L

Formal statement: ∀ε>0, ∃δ>0 such that 0 < |x-a| < δ ⟹ |f(x)-L| < ε

Step 1: Set Up the Framework

• • Identify f(x), a, and L
• • State what we need to prove
• • Write: "Let ε > 0 be given. We need to find δ > 0 such that..."

Template

Let ε > 0 be given.
We need to find δ > 0 such that:
  whenever 0 < |x - a| < δ, we have |f(x) - L| < ε.

Step 2: Work Backwards

• • Start with |f(x) - L|
• • Simplify and bound in terms of |x - a|
• • Find the relationship between ε and δ

Common Pattern

If |f(x) - L| ≤ C · |x - a| for some constant C, then choose δ = ε/C.

Step 3: Choose δ

Based on your analysis:

• • δ must be positive
• • δ may depend on ε
• • Sometimes need δ = min(1, ε/C) to handle multiple constraints

Step 4: Verify Forward

• • Assume 0 < |x - a| < δ
• • Show step-by-step that |f(x) - L| < ε
• • Each inequality must be justified

Step 5: Lean Formalization

-- Limit definition in Lean/Mathlib
-- Uses Filter.Tendsto and nhds (neighborhood)
import Mathlib.Topology.Basic

example (f : ℝ → ℝ) (a L : ℝ) :
    Filter.Tendsto f (nhds a) (nhds L) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| < δ → |f x - L| < ε := by
  sorry -- This is the relationship

Key tactics:

• •norm_num - numerical bounds
• •linarith - linear inequalities
• •nlinarith - nonlinear (limited)
• •abs_sub_abs_le_abs_sub - triangle inequality

Common Examples

Example 1: lim_{x→2} 3x = 6

• •|3x - 6| = 3|x - 2|
• •Choose δ = ε/3

Example 2: lim_{x→0} x² = 0

• •Need |x² - 0| < ε when |x| < δ
• •If |x| < 1 and |x| < √ε, then |x²| < ε
• •Choose δ = min(1, √ε)

Output Format

**Limit:** lim_{x→a} f(x) = L

**Proof:**

Let ε > 0 be given.
Choose δ = [formula].

Verification:
Suppose 0 < |x - a| < δ.
Then:
  |f(x) - L| = ...
            ≤ ...
            < ε ✓

Therefore, lim_{x→a} f(x) = L. ∎