analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
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 \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)$ and $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.
(classical IVT, assuming excluded middle)
Let $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) \lt 0$ while $f(b) \gt 0$. Then there exists a point $c$ in the unit interval such that $f(c) = 0$.
Let $g:\mathbb{R} \to \mathbb{R}$ be defined as $g(x) \coloneqq (b - a) x + a$. Then we can define a function $h:[0,1] \to \mathbb{R}$ by $h \coloneqq f \circ g$.
By this example the interval $[0,1]$ is a connected topological space (this is where excluded middle is used).
By this prop. also its image $f([0,1]) \subset \mathbb{R}$ is connected. By this example that image is itself an interval. This implies the claim is true for $h$. Since linear functions preserve the properties of an interval being compact and closed, if the claim is true for $h$, it is true for $f$.
(constructive IVT with weakened conclusion)
For real numbers $a$ and $b$, let $f\colon [a,b] \to \mathbb{R}$ be a pointwise continuous function from the closed interval $[a, b]$ to the real line, and supposed that $f(a) \lt 0$ and $f(b) \gt 0$. Then for every positive number $\epsilon$ there exists a point $c_\epsilon$ in the unit interval such that ${|f(c_\epsilon)|} \lt \epsilon$.
This proof originally appeared in Frank 2020.
Let us inductively define the following sequences:
Then
and the sequence $c_n$ is a Cauchy sequence, because for natural numbers $m \lt n$,
Lemma: For every natural number $m$, either 1. there exists a $j \leq m$ such that $\vert f(c_j) \lt \epsilon$, or 2. $f(a_m) \lt 0$ and $f(b_m) \gt 0$. This could be proved by induction on natural numbers:
When $m = 0$, $f(a_0) = f(a) \lt 0$ and $f(b_0) = f(b) \gt 0$.
Now, assume that the above lemma is true for a particular $m$. If there exists a $j \leq m$ such that $\vert f(c_j) \lt \epsilon$, then there exists a $j \leq m + 1$ such that $\vert f(c_j) \lt \epsilon$. Otherwise, either $2 f(c_m) \lt -\epsilon$, $2 f(c_m) \gt \epsilon$, or $\vert f(c_m) \vert \gt \epsilon$.
If $2 f(c_m) \lt -\epsilon$, then we define
so that $a_{m + 1} \lt 0$ and $b_{m + 1} \gt 0$.
If $2 f(c_m) \gt \epsilon$, then we define
so that $a_{m + 1} \lt 0$ and $b_{m + 1} \gt 0$.
If $\vert f(c_m) \vert \gt \epsilon$, then there exists a $j \leq m + 1$ such that $\vert f(c_j) \lt \epsilon$.
Thus, the above lemma is true.
Now, by pointwise continuity at $c$, let $\delta$ be such that $\vert x - y \vert \lt \delta$ implies $\vert f(x) - f(y)\vert \lt \epsilon$. Choose a natural number $m$ such that
If there exists a $j \leq m$ such that $\vert f(c_j) \lt \epsilon$, then the intermediate value is true. Otherwise, $f(a_m) \lt 0$ and $f(b_m) \gt 0$, and so
and so that means that
which means that $\vert f(c) \vert \lt \epsilon$.
If excluded middle is true, then the classical IVT follows from the above theorem:
By way of contradiction (applying the double negation law of classical logic), suppose that ${|f(c)|} \gt 0$ for every $c$ in $[0,1]$. Then the extra hypothesis of Theorem is certainly satisfied, so there exists some $c$ such that $f(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:
Let $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) \lt 0$ or $f(x) \gt 0$ for all $x \in [a,b]$. Then $f$ is either everywhere positive or everywhere negative.
This appeared in Bauer 2016.
(constructive IVT with strengthened hypothesis, assuming the interval endpoints and the zero have locators and that the function is locally nonzero)
For real numbers $a$ and $b$ with locators, let $f\colon [a,b] \to \mathbb{R}$ be a pointwise continuous function from the closed interval $[a, b]$ to the real line that is a locally nonzero function and that lifts to locators, and suppose that $f(a) \leq 0$ and $f(b) \geq 0$. Then, there exists a point $c$ in $[a, b]$ with a locator such that $f(c) = 0$.
(constructive IVT with strengthened hypothesis, assuming weak countable choice and that the function is locally nonzero)
Assuming weak countable choice, for real numbers $a$ and $b$, let $f\colon [a,b] \to \mathbb{R}$ be a pointwise continuous function from the closed interval $[a, b]$ to the real line that is a locally nonzero function, and suppose that $f(a) \leq 0$ and $f(b) \geq 0$. Then, there exists a point $c$ in $[a, b]$ with a locator such that $f(c) = 0$.
(constructive IVT with strengthened hypothesis, assuming weak countable choice and that the function is uniformly continuous)
Let $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) \lt 0$ while $f(1) \gt 0$. Suppose further that, for any points $a,b$ in the unit interval with $a \lt b$, there exists a point $c_{a,b}$ such that $a \lt c_{a,b} \lt b$ and ${|f(c_{a,b})|} \gt 0$. (In other words, the non-zero set $\{ c : {|f(c)|} \gt 0 \}$ is dense.) Then there exists a point $c$ in the unit interval such that $f(c) = 0$.
(constructive IVT with strengthened hypothesis, assuming that the function is strictly monotonic with $0$ strictly between $f(0)$ and $f(1)$)
Let $f\colon [0,1] \to \mathbb{R}$ be a strictly monotonic from the unit interval to the real line, and suppose that $f(0) \lt 0$ while $f(1) \gt 0$. Then there exists a point $c$ in the unit interval such that $f(c) = 0$.
We construct Dedekind cuts $L = \{y \in [0,1] \vert f(y) \lt 0\}$ and $U = \{z \in [0,1] \vert f(z) \gt 0\}$ and by the Dedekind completeness of the real numbers, there is a unique $x \in [0, 1]$ such that $y \lt x \lt z$.
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.