Product Rule for Limits

Lean formalization

This note’s $\varepsilon$ - $\delta$ proof is formalized in Lean 4 + Mathlib in Limits1Flow.lean, a flow-faithful development: it defines its own $\varepsilon$ - $\delta$ limit predicate Limit and proves the product rule from scratch in the same three steps used below, without calling Mathlib’s Filter.Tendsto.mul. To certify the statement really concerns the limit, it also proves Limit f a L is equivalent to Mathlib’s punctured-neighbourhood limit Tendsto f (𝓝[≠] a) (𝓝 L) (limit_iff_tendsto); that bridge is never used inside the product-rule proof. Each Lean proof dropdown below splices the corresponding declaration verbatim from the compiled source. Continuous integration runs lake build (which fails on any error or sorry), and the file is axiom-clean (propext, Classical.choice, Quot.sound).

Theorem (Product Rule for Limits).
If $\lim_{x \to a} f(x) = L$ and $\lim_{x \to a} g(x) = M$ (where $L, M \in \mathbb{R}$ ), then

\lim_{x \to a} [f(x) g(x)] = LM.

(1)

Limits1Flow.lean

/-- The note's ε–δ definition of `lim_{x→a} f(x) = L`. The hypothesis `0 < |x - a|` is the note's
`0 < |x - a|`, i.e. the deleted/punctured limit that ignores the value (if any) at `x = a`. -/
def Limit (f : ℝ → ℝ) (a L : ℝ) : Prop :=
  ∀ ε > 0, ∃ δ > 0, ∀ x, 0 < |x - a| → |x - a| < δ → |f x - L| < ε

Limits1Flow.lean

/-- The note's ε–δ limit is **exactly** Mathlib's punctured-neighbourhood limit
`Tendsto f (𝓝[≠] a) (𝓝 L)`, so the results below concern the genuine limit. -/
theorem limit_iff_tendsto : Limit f a L ↔ Tendsto f (𝓝[≠] a) (𝓝 L) := by
  rw [Metric.tendsto_nhdsWithin_nhds]
  constructor
  · intro h ε hε
    obtain ⟨δ, hδ, hx⟩ := h ε hε
    refine ⟨δ, hδ, fun x hxmem hxδ => ?_⟩
    rw [Real.dist_eq] at hxδ ⊢
    have hx0 : 0 < |x - a| :=
      abs_pos.mpr (sub_ne_zero.mpr (Set.mem_compl_singleton_iff.mp hxmem))
    exact hx x hx0 hxδ
  · intro h ε hε
    obtain ⟨δ, hδ, hx⟩ := h ε hε
    refine ⟨δ, hδ, fun x hx0 hxδ => ?_⟩
    have hxmem : x ∈ ({a}ᶜ : Set ℝ) :=
      Set.mem_compl_singleton_iff.mpr (sub_ne_zero.mp (abs_pos.mp hx0))
    have := hx hxmem (by rw [Real.dist_eq]; exact hxδ)
    rwa [Real.dist_eq] at this

Proof (using the $\varepsilon$ - $\delta$ definition).

Let $\varepsilon > 0$ be arbitrary. We must find $\delta > 0$ such that

0 < |x - a| < \delta \quad \implies \quad |f(x)g(x) - LM| < \varepsilon.

(2)

Step 1: Bound $|f(x)|$ near $a$ .
Since $\lim_{x \to a} f(x) = L$ , there exists $\delta_1 > 0$ such that

0 < |x - a| < \delta_1 \quad \implies \quad |f(x) - L| < 1.

(3)

Therefore,

|f(x)| = |f(x) - L + L| \leq |f(x) - L| + |L| < 1 + |L|.

(4)

Let $B := |L| + 1 > 0$ . Then $|f(x)| < B$ whenever $0 < |x - a| < \delta_1$ .

Limits1Flow.lean

/-- **Step 1.** A function with limit `L` at `a` is bounded by `|L| + 1` near `a`: taking `ε = 1`
gives `δ₁` with `|f x - L| < 1`, hence `|f x| ≤ |f x - L| + |L| < |L| + 1`. -/
theorem exists_bound_near (hf : Limit f a L) :
    ∃ δ₁ > 0, ∀ x, 0 < |x - a| → |x - a| < δ₁ → |f x| < |L| + 1 := by
  obtain ⟨δ₁, hδ₁, hx⟩ := hf 1 one_pos
  refine ⟨δ₁, hδ₁, fun x hx0 hxδ => ?_⟩
  have h1 : |f x - L| < 1 := hx x hx0 hxδ
  calc |f x| = |(f x - L) + L| := by congr 1; ring
    _ ≤ |f x - L| + |L| := abs_add_le _ _
    _ < 1 + |L| := by linarith
    _ = |L| + 1 := by ring

Step 2: Control the two terms in the product difference.
Rewrite the expression we want to bound:

|f(x)g(x) - LM| = |f(x)(g(x) - M) + M(f(x) - L)| \leq |f(x)| \cdot |g(x) - M| + |M| \cdot |f(x) - L|.

(5)

We will make each term on the right smaller than $\varepsilon/2$ .

Choose $\delta_2 > 0$ so that $|g(x) - M|$ is small enough:
Since $\lim_{x \to a} g(x) = M$ , there exists $\delta_2 > 0$ such that
$0 < |x - a| < \delta_2 \quad \implies \quad |g(x) - M| < \frac{\varepsilon}{2B}.$
(6)

Then the first term satisfies
$|f(x)| \cdot |g(x) - M| < B \cdot \frac{\varepsilon}{2B} = \frac{\varepsilon}{2}.$
(7)
Choose $\delta_3 > 0$ so that $|f(x) - L|$ is small enough:
Since $\lim_{x \to a} f(x) = L$ , there exists $\delta_3 > 0$ such that
$0 < |x - a| < \delta_3 \quad \implies \quad |f(x) - L| < \frac{\varepsilon}{2(|M| + 1)}.$
(8)

Then the second term satisfies
$|M| \cdot |f(x) - L| < |M| \cdot \frac{\varepsilon}{2(|M| + 1)} = \frac{|M|}{2(|M| + 1)} \varepsilon < \frac{\varepsilon}{2},$
(9)

because $\frac{|M|}{|M| + 1} < 1$ for any finite real number $M$ .

Step 3: Choose the overall $\delta$ .
Let

\delta := \min\{\delta_1, \delta_2, \delta_3\} > 0.

(10)

Now suppose $0 < |x - a| < \delta$ . Then all three conditions hold simultaneously:

$|f(x)| < B$ ,
$|g(x) - M| < \frac{\varepsilon}{2B}$ ,
$|f(x) - L| < \frac{\varepsilon}{2(|M| + 1)}$ .

Therefore,

|f(x)g(x) - LM| < \frac{\varepsilon}{2} + \frac{\varepsilon}{2} = \varepsilon.

(11)

This completes the proof. (The case $M = 0$ is covered automatically, since the second term vanishes or is even smaller.)

Limits1Flow.lean

/-- **Product rule for limits.** If `lim f = L` and `lim g = M` at `a`, then `lim (f·g) = L·M`.
Proved straight from the ε–δ definition as in the note: bound `|f|` by `B = |L| + 1`, force each of
the two terms below `ε/2`, and take `δ = min{δ₁, δ₂, δ₃}`. -/
theorem limit_mul (hf : Limit f a L) (hg : Limit g a M) :
    Limit (fun x => f x * g x) a (L * M) := by
  intro ε hε
  -- Step 1: bound |f| by B = |L| + 1.
  obtain ⟨δ₁, hδ₁, hbound⟩ := exists_bound_near hf
  set B : ℝ := |L| + 1 with hB
  have hBpos : 0 < B := by positivity
  -- Step 2: control each term: |g - M| < ε/(2B) and |f - L| < ε/(2(|M|+1)).
  obtain ⟨δ₂, hδ₂, hg2⟩ := hg (ε / (2 * B)) (by positivity)
  obtain ⟨δ₃, hδ₃, hf3⟩ := hf (ε / (2 * (|M| + 1))) (by positivity)
  -- Step 3: choose δ = min{δ₁, δ₂, δ₃}.
  refine ⟨min δ₁ (min δ₂ δ₃), by positivity, fun x hx0 hxδ => ?_⟩
  have hx1 : |x - a| < δ₁ := lt_of_lt_of_le hxδ (min_le_left _ _)
  have hx2 : |x - a| < δ₂ := lt_of_lt_of_le hxδ ((min_le_right _ _).trans (min_le_left _ _))
  have hx3 : |x - a| < δ₃ := lt_of_lt_of_le hxδ ((min_le_right _ _).trans (min_le_right _ _))
  have hfb : |f x| < B := hbound x hx0 hx1
  have hgm : |g x - M| < ε / (2 * B) := hg2 x hx0 hx2
  have hfl : |f x - L| < ε / (2 * (|M| + 1)) := hf3 x hx0 hx3
  -- term 1: |f x| · |g x - M| < ε/2.
  have ht1 : |f x| * |g x - M| < ε / 2 := by
    calc |f x| * |g x - M| ≤ B * |g x - M| := by gcongr
      _ < B * (ε / (2 * B)) := by gcongr
      _ = ε / 2 := by field_simp
  -- term 2: |M| · |f x - L| ≤ ε/2.
  have ht2 : |M| * |f x - L| ≤ ε / 2 := by
    have step : |M| * |f x - L| ≤ (|M| + 1) * (ε / (2 * (|M| + 1))) :=
      mul_le_mul (by linarith [abs_nonneg M]) hfl.le (abs_nonneg _) (by positivity)
    calc |M| * |f x - L| ≤ (|M| + 1) * (ε / (2 * (|M| + 1))) := step
      _ = ε / 2 := by field_simp
  -- combine via the triangle inequality.
  have hsplit : f x * g x - L * M = f x * (g x - M) + M * (f x - L) := by ring
  calc |(fun x => f x * g x) x - L * M|
      = |f x * (g x - M) + M * (f x - L)| := by simp only [hsplit]
    _ ≤ |f x * (g x - M)| + |M * (f x - L)| := abs_add_le _ _
    _ = |f x| * |g x - M| + |M| * |f x - L| := by rw [abs_mul, abs_mul]
    _ < ε := by linarith

Note: The same technique works for one-sided limits and for limits at $\pm \infty$ (with appropriate modifications to the definition).