Interpolating Between Choices for the Approximate Intermediate Value Theorem

TL;DR

This paper proves the approximate intermediate value theorem constructively under weak hypotheses by interpolating between choices in a bisection-like algorithm, avoiding classical assumptions like uniform continuity and countable choice.

Contribution

It introduces a novel constructive proof of the approximate intermediate value theorem that interpolates between classical bisection choices, requiring only pointwise continuity and weak hypotheses.

Findings

Proves the approximate intermediate value theorem constructively.

Develops an interpolation method between classical bisection choices.

Avoids reliance on uniform continuity and countable choice.

Abstract

This paper proves the approximate intermediate value theorem, constructively and from notably weak hypotheses: from pointwise rather than uniform continuity, without assuming that reals are presented with rational approximants, and without using countable choice. The theorem is that if a pointwise continuous function has both a negative and a positive value, then it has values arbitrarily close to 0. The proof builds on the usual classical proof by bisection, which repeatedly selects the left or right half of an interval; the algorithm here selects an interval of half the size in a continuous way, interpolating between those two possibilities.

Equations

$$a_1=a$$

$$b_1=b$$

$$c_n=(a_n+b_n)/2$$

$$d_n=\max (0,\min (\frac{1}{2}+\frac{f(c_n)}{ϵ},1))$$

$$a_{n+1}=c_n-d_n(b-a)/2^n$$

$$b_{n+1}=b_n-d_n(b-a)/2^n$$

$$|c-a_m|\le |c-c_m|+|c_m-a_m|<\delta ,\text{ so }|f(c)-f(a_m)|<ϵ$$

$$|c-b_m|\le |c-c_m|+|c_m-b_m|<\delta ,\text{ so }|f(c)-f(b_m)|<ϵ$$

$$d_m=1$$

$$a_{m+1}=a_m,\text{ so }f(a_{m+1})<0$$

$$b_{m+1}=c_m,\text{ so }f(b_{m+1})>0$$

$$d_m=0$$

$$a_{m+1}=c_m,\text{ so }f(a_{m+1})<0$$

$$b_{m+1}=b_m,\text{ so }f(b_{m+1})>0$$

Full text

I thank Andrej Bauer, Mike Shulman and Bas Spitters for helpful dialogue on this topic.

1. Introduction

On MathOverflow [Shu16], Mike Shulman asked: “Can the approximate Intermediate Value Theorem be proven constructively about an arbitrary (pointwise) continuous function $f$, without using any form of choice or excluded middle (e.g. in the mathematics valid in any elementary topos with a natural numbers object)?”

Here, the approximate Intermediate Value Theorem is

Theorem 1**.**

If $f$ is pointwise continuous on $[a,b]$ and $f(a)<0<f(b)$, then for every $\epsilon>0$, there is some $x$ with $|f(x)|<\epsilon$.

The proof below answers “Yes” to Shulman’s question, satisfying four notable constraints. The first is that the proof should be constructive, in particular using only intuitionistic logic and not relying on the principle of excluded middle. This puts the standard intermediate value theorem, in which $f(x)=0$, out of reach [BR87, chapter 6.2].

The second constraint is that the proof should use pointwise rather than uniform continuity. Under uniform continuity, there is a $\delta$ corresponding to the $\epsilon$, there is a sequence of $x$’s going from $a$ to $b$ in steps of less than $\delta$, and one of those $x$’s will have $|f(x)|<\epsilon$. This is the proof in Bishop and Bridges [BB85, theorem 4.8, p. 40], but pointwise continuity does not constructively imply uniform continuity.

The third constraint is that the proof should not use countable choice. Under countable choice, it suffices in the proof below to let $d_{n}=0$ if $f(c_{n})<\epsilon$ or $d_{n}=1$ if $f(c_{n})>-\epsilon$, but without countable choice, such a sequence is ill-defined.

The fourth constraint is that the proof should not assume that reals are presented with rational approximants. If a real number is defined as a sequence of rationals, then $d_{n}$ can be defined as 0 if the $n^{th}$ rational approximation to $f(c_{n})$ is negative, or 1 otherwise. However, this operation does not respect the relation of equality on reals, and it is not appropriate for reals defined as Dedekind cuts.

The “yes” is qualified only by the need for real numbers to be defined so that Cauchy sequences of them converge in the topos. For instance, this result holds if reals are defined in the usual constructive way, as Cauchy sequences of rationals with specified modulus (i.e. sequences $q_{m}$ where $|q_{m}-q_{m^{\prime}}|<1/m+1/{m^{\prime}}$); or if reals are defined as Dedekind cuts [BR87, chapters 2.2 and 7.3]. However, this result may not hold if reals are defined as naive Cauchy sequences of rationals (i.e. sequences $q_{m}$ where for all $\epsilon$, for some $n$, for all $m>n$ and $m^{\prime}>n$, $|q_{m}-q_{m^{\prime}}|<\epsilon$), or if they are defined as equivalence classes [Sch03, notes 12-13].

The proof below satisfies all the constraints above, and works for topoi in which countable choice fails. It strengthens some of Schuster’s results [Sch03, section 5]. It can also apply to the case $f(a)\leq 0$, $f(b)\geq 0$ by changing strict to non-strict inequalities appropriately.

This proof reduces to the usual classical proof by bisection if the definition of $d_{n}$ is replaced by $d_{n}=0$ if $f(c_{n})<0$ and $d_{n}=1$ otherwise, choosing either the left half or the right half of the interval at each step. The key difference from that usual proof is that the algorithm here selects an interval of half the size in a continuous way, interpolating between those two possibilities.

2. Proof of the Theorem

Define the following inductively:

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

Then $b_{n}-a_{n}=(b-a)/2^{n-1}.$

So the $c_{n}$’s converge to some $c.$ In more detail: The $d_{n}$’s are between 0 and 1. Each interval $[a_{n+1},b_{n+1}]$ is of length $(b-a)/2^{n}$, and contained in the previous $[a_{n},b_{n}]$. The $c_{n}$ form a Cauchy sequence, since for $m<n$, $|c_{m}-c_{n}|\leq(b-a)/2^{m-1}$.

The following diagrams illustrate how an interval $[a_{n},b_{n}]$ and the value $f(c_{n})$ determine the next interval $[a_{n+1},b_{n+1}]$. High values of $f(c_{n})$ push the next interval to the left, and low values of $f(c_{n})$ push the next interval to the right.

f(c_{n})>\epsilon/2$$|f(c_{n})|<\epsilon/2$$f(c_{n})<-\epsilon/2$$\ \ \phantom{b}a_{n+1}$$\ \ \phantom{b}b_{n+1}$$\phantom{b}a_{n}$$\phantom{b}b_{n}$$\ \ \phantom{b}a_{n+1}$$\ \ \phantom{b}b_{n+1}$$\phantom{b}a_{n}$$\phantom{b}b_{n}$$\ \ \phantom{b}a_{n+1}$$\ \ \phantom{b}b_{n+1}$$\phantom{b}a_{n}$$\phantom{b}b_{n}

{clm}

For any $m\in\mathbb{N}$, either (i) $\exists j\leq m,\ |f(c_{j})|<\epsilon$ or (ii) $f(a_{m})<0$ and$f(b_{m})>0$.

• Proof of Theorem from Claim.

By pointwise continuity at $c$, let $\delta$ be such that $|x-c|<\delta$ implies $|f(x)-f(c)|<\epsilon.$ Choose $m$ such that $|c-c_{m}|<\delta/2$ and $(b-a)/2^{m}<\delta/2$, and apply the claim.

In the first case of the claim, the theorem is immediate.

In the second case of the claim,

[TABLE]

[TABLE]

So $f(c)$ is within $\epsilon$ of both a negative and a positive number, and $|f(c)|<\epsilon$.

• Proof of Claim, by induction on $m$.

The base case is given by $f(a)<0,\ f(b)>0.$

Now assume the claim for $m$. In case (i), for some $j<m,\ |f(c_{j})|<\epsilon$, and the inductive step is trivial.

In case (ii), use trichotomy with either $f(c_{m})<-\epsilon/2,\ |f(c_{m})|<\epsilon$, or $f(c_{m})>\epsilon/2.$

If $|f(c_{m})|<\epsilon$, then the inductive step is again trivial.

If $f(c_{m})>\epsilon/2$, then

[TABLE]

[TABLE]

[TABLE]

If $f(c_{m})<-\epsilon/2$, then

[TABLE]

[TABLE]

[TABLE]

This establishes the claim and the theorem. ∎

3. Comments and Examples

Note that $|f(c)|$ may be small or large. This is especially visible in the following diagrams, where $f$ is piecewise polynomial, the black dots show points $(c_{n},f(c_{n}))$, and the white squares show $(c,f(c))$.

The example below left starts from $[a,b]=[-1,1]$, $f(x)=\min(\frac{1+6x^{2}}{7},8+9x)$ and $(c_{1},f(c_{1}))=(0,1/7)$. Using $\epsilon=1/3$, the algorithm converges on $c=-0.8894$…. In this case $c$ is not quite the exact zero at $-8/9$, but the difference is below the scale of the graph, and $|f(c)|$ is well under $\epsilon$.

The example below right starts from the same initial data but with $\epsilon=1/2$. Then the algorithm converges on $c=-0.7485$…, for which $f(c)>\epsilon$. Taking $\delta=1/8$, $m=6$, the proof guarantees only that at least one of $f(c_{1}),\ldots,f(c_{6}),f(c)$ is within $\epsilon$ of zero, which is enough to show the approximate Intermediate Value Theorem.

1$$-1$$-1\phantom{-}$$1$$\epsilon=\frac{1}{3}$$1$$-1$$-1\phantom{-}$$1$$\epsilon=\frac{1}{2}