A Detailed Proof of a Limit Theorem

Manuel Kauers (TSW Homework)

December 17, 2002

Given the definition

∀_{{f \atop seq[f]}} (isConv[f] :⟷^{def.} ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f[n] − a| < ε)

we have to prove that

∀_{{f,g \atop seq[f],seq[g]}} isConv[f] ∧ isConv[g] → isConv[f + g].  (1)

We start with the claim as a single goal, and with no assuptions. (In fact, the assumptions contain the definition of convergence as well as the theory of arithmetics, but we will only state assumptions which appear during the proof in order to keep it readable.)

\frac{Ass:}{Goals: ∀_{{f,g \atop seq[f],seq[g]}} isConv[f] ∧ isConv[g] → isConv[f + g]}

At first, we eliminate the quantifier: “Let f and g be arbirtary but fixed sequences.”

Ass: seq[f_{0}], seq[g_{0}] ; Goals: isConv[f_{0}] ∧ isConv[g_{0}] → isConv[f_{0} + g_{0}]

Now, we add the lefthand side of the implication to the set of assumptions

Ass:  isConv[f_{0}] ∧ isConv[g_{0}],
seq[f_{0}], seq[g_{0}]
Goals: isConv[f_{0} + g_{0}]

We break the conjuction apart.

Ass:  isConv[f_{0}],
isConv[g_{0}],
seq[f_{0}], seq[g_{0}]
Goals: isConv[f_{0} + g_{0}]

We expand isConv into its definition.

Ass:  ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f_{0}[n] − a| < ε,

∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |g_{0}[n] − a| < ε,

seq[f_{0}], seq[g_{0}]

Goals: ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |(f_{0} + g_{0})[n] − a| < ε

Expand the existential quantifiers in the assumption:

Ass:  ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f_{0}[n] − a_{0}| < ε,

∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |g_{0}[n] − b_{0}| < ε,

seq[f_{0}], seq[g_{0}], a_{0} ∈ ℝ, b_{0} ∈ ℝ

Goals: ∃_{a∈ℝ} ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |(f_{0} + g_{0})[n] − a| < ε

Now the existential quantifier in the goal is initialized to a_{0} +b_{0} by educated guess. This introduces the additional goal that this sum is a real number.

Ass:  ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f_{0}[n] − a_{0}| < ε,

∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |g_{0}[n] − b_{0}| < ε,

seq[f_{0}], seq[g_{0}], a_{0} ∈ ℝ, b_{0} ∈ ℝ

Goals: ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |(f_{0} + g_{0})[n] − (a_{0} + b_{0})| < ε,

a_{0} + b_{0} ∈ ℝ

The quantifier in the goal is now eliminated by assuming an arbitrary but fixed constant as before.

Ass:  ∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f_{0}[n] − a_{0}| < ε,

∀_{{ε∈ℝ \atop ε>0}} ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |g_{0}[n] − b_{0}| < ε,

seq[f_{0}], seq[g_{0}], a_{0} ∈ ℝ, b_{0} ∈ ℝ, ε_{0} ∈ ℝ, ε_{0} > 0

Goals: ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |(f_{0} + g_{0})[n] − (a_{0} + b_{0})| < ε_{0},

a_{0} + b_{0} ∈ ℝ

The ε’s in the assumptions are initialized to ε_{0}/2 by educated guess.

Ass:  ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |f_{0}[n] − a_{0}| < ε_{0}/2,

∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |g_{0}[n] − b_{0}| < ε_{0}/2,

seq[f_{0}], seq[g_{0}], a_{0} ∈ ℝ, b_{0} ∈ ℝ, ε_{0} ∈ ℝ, ε_{0} > 0

Goals: ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |(f_{0} + g_{0})[n] − (a_{0} + b_{0})| < ε_{0},

a_{0} + b_{0} ∈ ℝ, ε_{0}/2 ∈ ℝ, ε_{0}/2 > 0

Let now N_{0}, M_{0} ∈ ℕ be arbirtary but fixed such that they fulfill the first two assumptions in order to eliminate the existential quantifiers there.

Ass:  ∀_{{n∈ℕ \atop n≥N_{0}}} |f_{0}[n] − a_{0}| < ε_{0}/2, ∀_{{n∈ℕ \atop n≥M_{0}}} |g_{0}[n] − b_{0}| < ε_{0}/2,

seq[f_{0}], seq[g_{0}], a_{0} ∈ ℝ, b_{0} ∈ ℝ, ε_{0} ∈ ℝ, ε_{0} > 0, N_{0} ∈ ℕ, M_{0} ∈ ℕ

Goals: ∃_{N∈ℕ} ∀_{{n∈ℕ \atop n≥N}} |(f_{0} + g_{0})[n] − (a_{0} + b_{0})| < ε_{0},
a_{0} + b_{0} ∈ ℝ, ε_{0}/2 ∈ ℝ, ε_{0}/2 > 0

Now, assuming N to be the maximum of N_{0} and M_{0} eliminates the existential quantifier of the main goal.

Ass:  ∀_{{n∈ℕ \atop n≥N_{0}}} |f_{0}[n] − a_{0}| < ε_{0}/2, ∀_{{n∈ℕ \atop n≥M_{0}}} |g_{0}[n] − b_{0}| < ε_{0}/2,

seq[f_{0}], seq[g_{0}], a_{0} ∈ ℝ, b_{0} ∈ ℝ, ε_{0} ∈ ℝ, ε_{0} > 0, N_{0} ∈ ℕ, M_{0} ∈ ℕ

Goals: ∀_{{n∈ℕ \atop n≥max\{N_{0},M_{0}\}}} |(f_{0} + g_{0})[n] − (a_{0} + b_{0})| < ε_{0},
a_{0} + b_{0} ∈ ℝ, ε_{0}/2 ∈ ℝ, ε_{0}/2 > 0, max{N_{0}, M_{0}}∈ℕ

Fix an arbitrary but fixed n_{0} ∈ ℕ with n_{0} ≥ max{N_{0}, M_{0}}. After that, initialize the n in the assumption to exacty this n_{0}.

Ass:  |f_{0}[n_{0}] − a_{0}| < ε_{0}/2, |g_{0}[n_{0}] − b_{0}| < ε_{0}/2,

seq[f_{0}], seq[g_{0}], a_{0} ∈ ℝ, b_{0} ∈ ℝ, ε_{0} ∈ ℝ, ε_{0} > 0, N_{0} ∈ ℕ, M_{0} ∈ ℕ,

n_{0} ∈ ℕ, n_{0} ≥ max{N_{0}, M_{0}}
Goals: |(f_{0} + g_{0})[n_{0}] − (a_{0} + b_{0})| < ε_{0},
a_{0} + b_{0} ∈ ℝ, ε_{0}/2 ∈ ℝ, ε_{0}/2 > 0, max{N_{0}, M_{0}}∈ℕ,
n_{0} ≥ N_{0}, n_{0} ≥ M_{0}

Application of the definition of (f_{0} + g_{0}) and some arithmetic axioms leads then to the following state:

Ass:  |f_{0}[n_{0}] − a_{0}| < ε_{0}/2, |g_{0}[n_{0}] − b_{0}| < ε_{0}/2,
seq[f_{0}], seq[g_{0}], a_{0} ∈ ℝ, b_{0} ∈ ℝ, ε_{0} ∈ ℝ, ε_{0} > 0, N_{0} ∈ ℕ,
M_{0} ∈ ℕ, n_{0} ∈ ℕ, n_{0} ≥ max{N_{0}, M_{0}}
Goals: |(f_{0}[n_{0}] − a_{0}) + (g_{0}[n_{0}] − b_{0})| < ε_{0},
a_{0} + b_{0} ∈ ℝ, ε_{0}/2 ∈ ℝ, ε_{0}/2 > 0, max{N_{0}, M_{0}}∈ℕ,
n_{0} ≥ N_{0}, n_{0} ≥ M_{0}

We insert an instance of the triangle inequality to the assumptions.

Ass:  |f_{0}[n_{0}] − a_{0}| < ε_{0}/2, |g_{0}[n_{0}] − b_{0}| < ε_{0}/2,
|(f_{0}[n_{0}] − a_{0}) + (g_{0}[n_{0}] − b_{0})| < |f_{0}[n_{0}] − a_{0}| + |g_{0}[n_{0}] − b_{0}|,
seq[f_{0}], seq[g_{0}], a_{0} ∈ ℝ, b_{0} ∈ ℝ, ε_{0} ∈ ℝ, ε_{0} > 0, N_{0} ∈ ℕ,
M_{0} ∈ ℕ, n_{0} ∈ ℕ, n_{0} ≥ max{N_{0}, M_{0}}
Goals: |(f_{0}[n_{0}] − a_{0}) + (g_{0}[n_{0}] − b_{0})| < ε_{0},
a_{0} + b_{0} ∈ ℝ, ε_{0}/2 ∈ ℝ, ε_{0}/2 > 0, max{N_{0}, M_{0}}∈ℕ,
n_{0} ≥ N_{0}, n_{0} ≥ M_{0}

Using the transitivity of < and a little bit of arithmetics using the assumptions around leads to

Ass:  |f_{0}[n_{0}] − a_{0}| < ε_{0}/2, |g_{0}[n_{0}] − b_{0}| < ε_{0}/2,
|(f_{0}[n_{0}] − a_{0}) + (g_{0}[n_{0}] − b_{0})| < |f_{0}[n_{0}] − a_{0}| + |g_{0}[n_{0}] − b_{0}|,
|(f_{0}[n_{0}] − a_{0}) + (g_{0}[n_{0}] − b_{0})| < ε_{0},
seq[f_{0}], seq[g_{0}], a_{0} ∈ ℝ, b_{0} ∈ ℝ, ε_{0} ∈ ℝ, ε_{0} > 0, N_{0} ∈ ℕ,
M_{0} ∈ ℕ, n_{0} ∈ ℕ, n_{0} ≥ max{N_{0}, M_{0}}
Goals: |(f_{0}[n_{0}] − a_{0}) + (g_{0}[n_{0}] − b_{0})| < ε_{0},
a_{0} + b_{0} ∈ ℝ, ε_{0}/2 ∈ ℝ, ε_{0}/2 > 0, max{N_{0}, M_{0}}∈ℕ,
n_{0} ≥ N_{0}, n_{0} ≥ M_{0}

We can now delete the main goal as it appears on both sides (because A → A is a tautology):

Ass:  |f_{0}[n_{0}] − a_{0}| < ε_{0}/2, |g_{0}[n_{0}] − b_{0}| < ε_{0}/2,
|(f_{0}[n_{0}] − a_{0}) + (g_{0}[n_{0}] − b_{0})| < |f_{0}[n_{0}] − a_{0}| + |g_{0}[n_{0}] − b_{0}|,
seq[f_{0}], seq[g_{0}], a_{0} ∈ ℝ, b_{0} ∈ ℝ, ε_{0} ∈ ℝ, ε_{0} > 0, N_{0} ∈ ℕ,
M_{0} ∈ ℕ, n_{0} ∈ ℕ, n_{0} ≥ max{N_{0}, M_{0}}
Goals: a_{0} + b_{0} ∈ ℝ, ε_{0}/2 ∈ ℝ, ε_{0}/2 > 0, max{N_{0}, M_{0}}∈ℕ,
n_{0} ≥ N_{0}, n_{0} ≥ M_{0}

The remaining goals do not really belong to the limit theorem, but rather to basic arithmetics. We don’t want to prove them here. .