Limit

From CS2800 wiki

We won't study limits in this course (indeed, they are very non-discrete!), but this example demonstrates that the basic logical tools we study are used to define continuous concepts like limits.

We can use deeply quantified statements to defined complicated concepts like limits. The idea behind the limit of a function is that one can force the function's output to be equal to the limit at [math]x_0 [/math] (within any given tolerance) by making the input sufficiently close to [math]x_0 [/math]. This can be formalized as follows:

If [math]f [/math] is a function from [math]\href{/cs2800/wiki/index.php?title=Real_number&action=edit&redlink=1}{\mathbb{R}} [/math] to [math]\href{/cs2800/wiki/index.php?title=Real_number&action=edit&redlink=1}{\mathbb{R}} [/math], we say that the limit of [math]f [/math] at [math]x_0 [/math] is [math]a [/math] (written [math]\href{/cs2800/wiki/index.php/%5Clim}{\lim}_{x → x_0} f = a [/math]) if for all tolerances [math]ε \gt 0 [/math], there exists a distance [math]δ \gt 0 [/math] such that for any value [math]x [/math] that is within the range [math](x_0 - δ, x_0 + δ) [/math], the distance between [math]f(x) [/math] and [math]a [/math] is smaller than the tolerance.

More concisely, [math]\href{/cs2800/wiki/index.php/%5Clim}{\lim}_{x → x_0} f = a [/math] means [math]\href{/cs2800/wiki/index.php/%E2%88%80}{∀} ε \gt 0, \href{/cs2800/wiki/index.php/%E2%88%83}{∃} δ \lt 0, \href{/cs2800/wiki/index.php/%E2%88%80}{∀} x, \text{ if } 0 \lt |x - x_0| \lt δ \text{ then } |f(x) - a| \lt ε [/math].

Since we have a formal definition using standard logical constructs, we can use our usual proof techniques to prove things about limits:

[math]\href{/cs2800/wiki/index.php/%5Clim}{\lim}_{x → 0} f = 0 [/math] where [math]f(x) := x [/math].
Proof:
We want to show that [math]\href{/cs2800/wiki/index.php/%E2%88%80}{∀} ε \gt 0, \href{/cs2800/wiki/index.php/%E2%88%83}{∃} δ \gt 0, \href{/cs2800/wiki/index.php/%E2%88%80}{∀} x, \text{ if } 0 \lt |x - 0| \lt δ \text{ then } |f(x) - 0| \lt ε [/math].


Choose an arbitrary [math]ε \gt 0 [/math]. Let [math]δ \href{/cs2800/wiki/index.php/Definition}{:=} ε [/math] ([math]δ \gt 0 [/math] since [math]ε \gt 0 [/math]). Choose an arbitrary [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%E2%84%9D&action=edit&redlink=1}{ℝ} [/math], and assume that [math]0 \lt |x - x_0| \lt δ [/math]. We want to show that [math]|f(x) - 0| \lt ε [/math].


Well, by definition, [math]f(x) = x [/math], and by assumption, we have [math]0 \lt |x - x_0| \lt δ [/math]. But [math]ε = δ [/math] by definition; therefore [math]|f(x) - x_0| = |x - x_0| \lt δ = ε [/math] as required.

In this example, you might conclude that since the limit is [math]0 [/math], it cannot be 1. But this assumes that the limit is unique. We can directly prove that the limit is not 1 by proving the logical negation of the fact that the limit is 1:

[math]\href{/cs2800/wiki/index.php/%5Clim}{\lim}_{x → 0} f \neq 1 [/math] where [math]f(x) := x [/math].
Proof:
The logical negation of

[math]\href{/cs2800/wiki/index.php/%E2%88%80}{∀} ε \gt 0, \href{/cs2800/wiki/index.php/%E2%88%83}{∃} δ \gt 0, \href{/cs2800/wiki/index.php/%E2%88%80}{∀} x, \text{ if } 0 \lt |x - 0| \lt δ \text{ then } |f(x) - 1| \lt ε [/math]

is

[math]\href{/cs2800/wiki/index.php/%E2%88%83}{∃} ε \gt 0, \href{/cs2800/wiki/index.php/%E2%88%80}{∀} δ \gt 0, \href{/cs2800/wiki/index.php/%E2%88%83}{∃} x, 0 \lt |x - 0| \lt δ \text{ and } |f(x) - 1| \not\lt ε [/math]

Let [math]ε = 1/2 [/math]. Choose an arbitrary [math]δ \gt 0 [/math].

Let [math]x [/math] be the minimum of [math]δ/2 [/math] and [math]1/2 [/math]. Note that [math]0 \lt x [/math], [math]x \leq δ/2 [/math] and [math]x \leq 1/2 [/math] (you can prove this using case analysis).

Then we have [math]0 \lt x \leq δ/2 \lt δ [/math]. Moreover, [math]x ≤ 1/2 [/math] so [math]f(x) - 1 \leq 1/2 - 1 \leq -1/2 [/math], and therefore [math]|f(x) - 1| \geq 1/2 = ε [/math], which is what we were trying to prove.