nLab intermediate value theorem

The intermediate value theorem

The intermediate value theorem

Idea

The intermediate value theorem (IVT) is a fundamental principle of analysis which allows one to find a desired value by interpolation. It says that a continuous function f:[0,1]f \colon [0,1] \to \mathbb{R} from an interval to the real numbers (all with its Euclidean topology) takes all values in between f(0)f(0) and f(1)f(1).

The IVT in its general form was not used by Euclid. Although it is hard to doubt that Euclid believed that, for any given angle, there was an angle with one-third the measure, this angle cannot be constructed by the methods available to Euclid, so he would never refer to it (see at Euclidean geometry). In contrast, Archimedes made general arguments in which a quantity is approached from above and below, allowing him not only to trisect the angle but also to calculate π.

As normally stated, the IVT is not valid in constructive mathematics, although there are constructively valid versions. These versions either weaken the conclusion to an approximate zero, or to strengthen the hypothesis to require the functions satisfy additional properties or have other structures, such as locally nonconstancy and lifting to locators in functions in the given example below. Even interpreted classically, these are prima facie weaker results.

Statements and Proofs

Classical IVT

Theorem

(classical IVT, assuming excluded middle)

Let f:[a,b]f\colon [a,b] \to \mathbb{R} be a continuous function from a compact closed interval to the real line, and suppose that f(a)<0f(a) \lt 0 while f(b)>0f(b) \gt 0. Then there exists a point cc in the unit interval such that f(c)=0f(c) = 0.

Proof

Let g:g:\mathbb{R} \to \mathbb{R} be defined as g(x)(ba)x+ag(x) \coloneqq (b - a) x + a. Then we can define a function h:[0,1]h:[0,1] \to \mathbb{R} by hfgh \coloneqq f \circ g.

By this example the interval [0,1][0,1] is a connected topological space (this is where excluded middle is used).

By this prop. also its image f([0,1])f([0,1]) \subset \mathbb{R} is connected. By this example that image is itself an interval. This implies the claim is true for hh. Since linear functions preserve the properties of an interval being compact and closed, if the claim is true for hh, it is true for ff.

Constructive IVT with weakened conclusion

Theorem

(constructive IVT with weakened conclusion)

For real numbers aa and bb, let f:[a,b]f\colon [a,b] \to \mathbb{R} be a pointwise continuous function from the closed interval [a,b][a, b] to the real line, and supposed that f(a)<0f(a) \lt 0 and f(b)>0f(b) \gt 0. Then for every positive number ϵ\epsilon there exists a point c ϵc_\epsilon in the unit interval such that |f(c ϵ)|<ϵ{|f(c_\epsilon)|} \lt \epsilon.

Proof of Theorem

This proof originally appeared in Frank 2020.

Let us inductively define the following sequences:

a 0aa_0 \coloneqq a
b 0bb_0 \coloneqq b
c na n+b n2c_n \coloneqq \frac{a_n + b_n}{2}
d nmax(0,min(12+f(c ϵ)ϵ,1))d_n \coloneqq \max\left(0, \min\left(\frac{1}{2} + \frac{f(c_\epsilon)}{\epsilon}, 1\right)\right)
a n+1=c nd n(ba)2 n+1a_{n + 1} = c_n - \frac{d_n (b - a)}{2^{n + 1}}
a n+1=b nd n(ba)2 n+1a_{n + 1} = b_n - \frac{d_n (b - a)}{2^{n + 1}}

Then

b na n=ba2 nb_n - a_n = \frac{b - a}{2^n}

and the sequence c nc_n is a Cauchy sequence, because for natural numbers m<nm \lt n,

|c mc n|ba2 m\vert c_m - c_n \vert \leq \frac{b - a}{2^m}

Lemma: For every natural number mm, either 1. there exists a jmj \leq m such that |f(c j)<ϵ\vert f(c_j) \lt \epsilon, or 2. f(a m)<0f(a_m) \lt 0 and f(b m)>0f(b_m) \gt 0. This could be proved by induction on natural numbers:

When m=0m = 0, f(a 0)=f(a)<0f(a_0) = f(a) \lt 0 and f(b 0)=f(b)>0f(b_0) = f(b) \gt 0.

Now, assume that the above lemma is true for a particular mm. If there exists a jmj \leq m such that |f(c j)<ϵ\vert f(c_j) \lt \epsilon, then there exists a jm+1j \leq m + 1 such that |f(c j)<ϵ\vert f(c_j) \lt \epsilon. Otherwise, either 2f(c m)<ϵ2 f(c_m) \lt -\epsilon, 2f(c m)>ϵ2 f(c_m) \gt \epsilon, or |f(c m)|>ϵ\vert f(c_m) \vert \gt \epsilon.

  • If 2f(c m)<ϵ2 f(c_m) \lt -\epsilon, then we define

    d m1d_m \coloneqq 1
    a m+1a ma_{m + 1} \coloneqq a_m
    b m+1c mb_{m + 1} \coloneqq c_m

    so that a m+1<0a_{m + 1} \lt 0 and b m+1>0b_{m + 1} \gt 0.

  • If 2f(c m)>ϵ2 f(c_m) \gt \epsilon, then we define

    d m1d_m \coloneqq 1
    a m+1c ma_{m + 1} \coloneqq c_m
    b m+1b mb_{m + 1} \coloneqq b_m

    so that a m+1<0a_{m + 1} \lt 0 and b m+1>0b_{m + 1} \gt 0.

  • If |f(c m)|>ϵ\vert f(c_m) \vert \gt \epsilon, then there exists a jm+1j \leq m + 1 such that |f(c j)<ϵ\vert f(c_j) \lt \epsilon.

Thus, the above lemma is true.

Now, by pointwise continuity at cc, let δ\delta be such that |xy|<δ\vert x - y \vert \lt \delta implies |f(x)f(y)|<ϵ\vert f(x) - f(y)\vert \lt \epsilon. Choose a natural number mm such that

|cc m|<δ2\vert c - c_m \vert \lt \frac{\delta}{2}
|ba|2 m+1<δ2\frac{\vert b - a \vert}{2^{m + 1}} \lt \frac{\delta}{2}

If there exists a jmj \leq m such that |f(c j)<ϵ\vert f(c_j) \lt \epsilon, then the intermediate value is true. Otherwise, f(a m)<0f(a_m) \lt 0 and f(b m)>0f(b_m) \gt 0, and so

|cc m|<|cc m|+|c ma m|<δ\vert c - c_m \vert \lt \vert c - c_m \vert + \vert c_m - a_m \vert \lt \delta
|cc m|<|cc m|+|c mb m|<δ\vert c - c_m \vert \lt \vert c - c_m \vert + \vert c_m - b_m \vert \lt \delta

and so that means that

|f(c)f(a m)|<ϵ\vert f(c) - f(a_m) \vert \lt \epsilon
|f(c)f(b m)|<ϵ\vert f(c) - f(b_m) \vert \lt \epsilon

which means that |f(c)|<ϵ\vert f(c) \vert \lt \epsilon.

If excluded middle is true, then the classical IVT follows from the above theorem:

Proof of Theorem

By way of contradiction (applying the double negation law of classical logic), suppose that |f(c)|>0{|f(c)|} \gt 0 for every cc in [0,1][0,1]. Then the extra hypothesis of Theorem is certainly satisfied, so there exists some cc such that f(c)=0f(c) = 0 after all. (Constructively, this is enough to show that the classical theorem has no counterexample.)

There is also another constructively valid version of the IVT, where the conclusion is classically the contrapositive of the classical IVT, but which is weaker constructively since the reverse contrapositive rule does not hold constructively:

Theorem

Let f:[a,b]f\colon [a,b] \to \mathbb{R} be a continuous function from a compact closed interval to the real line, and suppose that f(x)<0f(x) \lt 0 or f(x)>0f(x) \gt 0 for all x[a,b]x \in [a,b]. Then ff is either everywhere positive or everywhere negative.

This appeared in Bauer 2016.

Constructive IVT with strengthened hypothesis

Theorem

(constructive IVT with strengthened hypothesis, assuming the interval endpoints and the zero have locators and that the function is locally nonzero)

For real numbers aa and bb with locators, let f:[a,b]f\colon [a,b] \to \mathbb{R} be a pointwise continuous function from the closed interval [a,b][a, b] to the real line that is a locally nonzero function and that lifts to locators, and suppose that f(a)0f(a) \leq 0 and f(b)0f(b) \geq 0. Then, there exists a point cc in [a,b][a, b] with a locator such that f(c)=0f(c) = 0.

Proof of Theorem

This proof originally appeared in Booij 2018

Theorem

(constructive IVT with strengthened hypothesis, assuming weak countable choice and that the function is locally nonzero)

Assuming weak countable choice, for real numbers aa and bb, let f:[a,b]f\colon [a,b] \to \mathbb{R} be a pointwise continuous function from the closed interval [a,b][a, b] to the real line that is a locally nonzero function, and suppose that f(a)0f(a) \leq 0 and f(b)0f(b) \geq 0. Then, there exists a point cc in [a,b][a, b] with a locator such that f(c)=0f(c) = 0.

Theorem

(constructive IVT with strengthened hypothesis, assuming weak countable choice and that the function is uniformly continuous)

Let f:[0,1]f\colon [0,1] \to \mathbb{R} be a uniformly continuous function from the unit interval to the real line, and suppose that f(0)<0f(0) \lt 0 while f(1)>0f(1) \gt 0. Suppose further that, for any points a,ba,b in the unit interval with a<ba \lt b, there exists a point c a,bc_{a,b} such that a<c a,b<ba \lt c_{a,b} \lt b and |f(c a,b)|>0{|f(c_{a,b})|} \gt 0. (In other words, the non-zero set {c:|f(c)|>0}\{ c : {|f(c)|} \gt 0 \} is dense.) Then there exists a point cc in the unit interval such that f(c)=0f(c) = 0.

Theorem

(constructive IVT with strengthened hypothesis, assuming that the function is strictly monotonic with 00 strictly between f(0)f(0) and f(1)f(1))

Let f:[0,1]f\colon [0,1] \to \mathbb{R} be a strictly monotonic from the unit interval to the real line, and suppose that f(0)<0f(0) \lt 0 while f(1)>0f(1) \gt 0. Then there exists a point cc in the unit interval such that f(c)=0f(c) = 0.

Proof

We construct Dedekind cuts L={y[0,1]|f(y)<0}L = \{y \in [0,1] \vert f(y) \lt 0\} and U={z[0,1]|f(z)>0}U = \{z \in [0,1] \vert f(z) \gt 0\} and by the Dedekind completeness of the real numbers, there is a unique x[0,1]x \in [0, 1] such that y<x<zy \lt x \lt z.

See also

References

  • Peter Schuster?; Unique existence, approximate solutions,

    and countable choice; doi.

  • Matt F.; answer to Approximate intermediate value theorem in pure constructive mathematics; MathOverflow; web.

  • Matthew Frank?, Interpolating Between Choices for the Approximate Intermediate Value Theorem (arxiv:1701.02227), Logical Methods in Computer Science, July 14, 2020, Volume 16, Issue 3 - doi:10.23638/LMCS-16(3:5)2020

  • Paul Taylor; The intermediate value theorem; A lambda calculus for real analysis, 14; web.

  • Auke Booij, Extensional constructive real analysis via locators, (abs:1805.06781)

  • Andrej Bauer, Five Stages of Accepting Constructive Mathematics, Bulletin of the American Mathematical Society, Volume 54, Number 3, July 2017, Pages 481–498. (doi:10.1090/bull/1556, pdf)

On the intermediate value theorem in cohesive homotopy type theory, see:

Last revised on February 19, 2024 at 12:40:51. See the history of this page for a list of all contributions to it.