nLab
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?. Roughly speaking, it says that if Papa Bear's porridge is too hot and Mama Bear's porridge is too cold, then there must be some temperature of porridge which is just right.

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. 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.

I've decided that I don't really like how I've been writing this, and I'm working on a new version. (Aside from its intrinsic interest and practical usefulness, this is such a classic example of the differences between classical and constructive analysis that I want to get it right.) That shouldn't stop anybody from putting here what they find useful, but I thought that a warning might be in order. —Toby Bartels

Statements

Theorem

(classical IVT, assuming excluded middle)

Let f:[0,1]f\colon [0,1] \to \mathbb{R} be a 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. Then there exists a point cc in the unit interval such that f(c)=0f(c) = 0.

Theorem

(constructive IVT with weakened conclusion)

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. 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.

Theorem

(constructive IVT with strengthened hypothesis, assuming weak countable choice)

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.

In the constructive versions, we have changed from a continuous function to a uniformly continuous one just to be safe; while some varieties of constructive analysis accept the theorem that any continous function on [0,1][0,1] is uniformly continous, others do not, and some even refute it. In any case, even the classical version only applies to uniformly continuous functions, even though the classical mathematician is free to leave out the word ‘uniformly’ and so usually does. The more significant change is to either weaken the conclusion to an approximate zero, or to strengthen the hypothesis to forbid functions that ‘hover’ near zero on some subinterval; even interpreted classically, these are prima facie weaker results.

There are obvious generalisations in which the domain [0,1][0,1] is generalised to any compact interval, in which the signs of f(0)f(0) and f(1)f(1) are swapped, and in which the desired value f(c)=0f(c) = 0 is generalised to any real number. They may be proved either by modifying a proof of the main theorem or as a corollary by linearly transforming the input and output of ff.

Proofs

We will prove Theorem 2 in a constructive manner, which (besides satisfying the constructive mathematicians) demonstrates an algorithm for approximating the point cc as closely as desired. Theorems 1 and 3 are then easy to prove (the latter constructively, the former not) as corollaries.

Proof of Theorem 2

Since ff is uniformly continuous, there exists a positive number δ\delta such that |f(x)f(y)|<ϵ/2{|f(x) - f(y)|} \lt \epsilon/2 whenever |xy|<δ{|x - y|} \lt \delta. Since δ\delta is positive, there exists a natural number nn such that δ>2 n\delta \gt 2^{-n}. We will approximate c ϵc_\epsilon in nn steps.

We will define finite sequences (a 1,,a n)(a_1,\ldots,a_n), (b 1,,b n)(b_1,\ldots,b_n), and (c 1,,c n)(c_1,\ldots,c_n) such that a k<c k<b ka_k \lt c_k \lt b_k at each stage. To begin with, let a 10a_1 \coloneqq 0 and b 11b_1 \coloneqq 1. At each stage, let c kc_k be the arithmetic mean of a ka_k and b kb_k. By the comparison property of the linear order <\lt, either f(c k)>ϵ/2f(c_k) \gt -\epsilon/2 or f(c k)<ϵ/2f(c_k) \lt \epsilon/2;

  • if the former, then let a k+1a ka_{k+1} \coloneqq a_k and b k+1c kb_{k+1} \coloneqq c_k,
  • if the latter, then let a k+1c ka_{k+1} \coloneqq c_k and b k+1b kb_{k+1} \coloneqq b_k.

Either way, we have a k+1<b k+1a_{k+1} \lt b_{k+1}, so we can continue.

At each stage, we have

  • f(a k)<ϵ/2f(a_k) \lt \epsilon/2,
  • f(b k)>ϵ/2f(b_k) \gt - \epsilon/2,
  • c ka k=2 kc_k - a_k = 2^k,
  • b kc k=2 kb_k - c_k = 2^k.

Therefore, ϵ<f(b n)ϵ/2<f(c n)<f(a k)+ϵ/2<ϵ-\epsilon \lt f(b_n) - \epsilon/2 \lt f(c_n) \lt f(a_k) + \epsilon/2 \lt \epsilon, so c nc_n is the c ϵc_\epsilon desired.

This is the bisection algorithm in numerical analysis?. Note that this algorithm always chooses c ϵc_\epsilon to be a dyadic rational?. Slight variations will allow c ϵc_\epsilon to be drawn from any previously chosen dense subspace of [0,1][0,1] (or this can be proved as a corollary).

Proof of Theorem 3

Suppose that ff satisfies the additional hypothesis (and assume weak countable choice).

I'm not sure how to finish this, and maybe it's a mistake! Certainly the result follows from countable choice, but I had thought that it followed from weak countable choice. (The proof from countable choice is to continue the bisection algorithm for infinitely many steps and take lim nc n\lim_n c_n.) There certainly ought to be a proof that uses only excluded middle (which implies WCCWCC), since Theorem 1 needs only that.

Proof of Theorem 1

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 3 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.)

Of course, we can also prove Theorems 1 and 3 directly by modifying the proof of Theorem 2 appropriately.

Other ways to identify cc (in Theorem 1 or 3) are as the supremum of {x|f(x)<0}\{x \;|\; f(x) \lt 0\} and using the extreme value theorem? as the minimum value of |f|{|f|}. (After accepting these non-constructive results, the proof that the value cc so found satisfies f(c)=0f(c) = 0, while perhaps non-trivial, is constructive without choice, given continuity and the extra hypothesis of Theorem 3.)

Revised on December 16, 2013 09:57:13 by Toby Bartels (64.89.53.106)