BTW, Colin, I was having some trouble with my email when I wrote this, which is why I didn't reply to your email directly (even to point you here). Sorry that I didn't correct that later.

]]>We have extended this approach to higher derivatives here. This uses the Hermite-Genocchi formula.

]]>@Colin The paper by Stolzenberg and Bridger that I link too presents a constructive approach to these issues that is works more smoothly classically too.

]]>You may enjoy this paper on the law of bounded change. Bridges also has a nice book on the topic.

]]>I was asked by email whether it is constructively provable that $f' = 0$ implies that $f$ is locally constant. (This is *not* the Mean Value Theorem, but that's related, and it came up.) The answer may depend on how one defines $f'$ in a constructive context, but it really should be Yes for any reasonable definition.

Ideally, I would take the pointwise definition. So, for every $x \in [0,1]$, we have a real number $f(x)$; and for $c \in [0,1]$, for every $\epsilon \gt 0$, for some $\delta \gt 0$, for every $x \in [0,1]$, whenever $0 \lt {|c - x|} \lt \delta$, we have ${|f(x) - f(c)|} \lt \epsilon {|x - c|}$. This is very weak; many constructivists would be inclined to add further structure or properties to $f$, but they should surely all agree that a differentiable function $f\colon [0,1] \to \mathbb{R}$ with $f' = 0$ has this much.

However, I can't quite make it work with this. From experience, I suspect that we need the fan theorem to make this work; otherwise, we need a stronger notion of *uniform* differentiability. This simply reverses the order of the quantifiers on $\delta$ and $c$; so, for every $\epsilon \gt 0$, for some $\delta \gt 0$, for every $c \in [0,1]$, for every $x \in [0,1]$, whenever $0 \lt {|x - c|} \lt \delta$, we have ${|f(x) - f(c)|} \lt \epsilon {|x - c|}$. Now I can make it work.

We wish to prove that $f(0) = f(1)$. (The general result follows upon composition with an affine linear function, which is trivial to handle.) Since equality of real numbers is the negation of apartness, we are allowed to prove this by contradiction, assuming that $f(0) \ne f(1)$; without loss of generality, assume that $f(0) \lt f(1)$. Let $f(1) - f(0)$ be $\epsilon$ and find a corresponding $\delta$. Find a natural number $n$ such that $n \gt 1/\delta$, and let $c_i = i/n$ for $i = 0, 1, 2, \ldots, n$. Then ${|c_{i+1} - c_i|} = 1/n \lt \delta$, so ${|f(c_{i+1}) - f({c_i})|} \lt \epsilon {|c_{i+1} - c_i|} = \epsilon/n$, so $f(c_{i+1}) - f({c_i}) \lt \epsilon/n$, so $\epsilon = f(1) - f(0) = \sum_i (f(c_{i+1}) - f({c_i})) \lt \sum_i (\epsilon/n) = \epsilon$; contradiction. QED.

]]>