## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorTobyBartels
• CommentTimeDec 28th 2013

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.

• CommentRowNumber2.
• CommentAuthorspitters
• CommentTimeDec 28th 2013

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

• CommentRowNumber3.
• CommentAuthorColin Tan
• CommentTimeDec 30th 2013
Thank you Toby for answering my question. I am happy to assume uniform differentiability. I notice many atimes constructive arguments rely on uniformity of continuity/differentiability etc. It makes me wonder why classical analysts do not show that compactness of domain implies uniformity and rely on these arguments.
• CommentRowNumber4.
• CommentAuthorspitters
• CommentTimeDec 30th 2013

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

• CommentRowNumber5.
• CommentAuthorColin Tan
• CommentTimeDec 30th 2013
Thank you. I will need to read this paper by Bridger and Stolzenberg in detail.
• CommentRowNumber6.
• CommentAuthorspitters
• CommentTimeDec 30th 2013

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

• CommentRowNumber7.
• CommentAuthorTobyBartels
• CommentTimeJan 2nd 2014

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.

• CommentRowNumber8.
• CommentAuthorColin Tan
• CommentTimeJan 20th 2014
No problem, Toby. Thanks for answering my question.