Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorTobyBartels
   • CommentTimeDec 28th 2013
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI 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.

   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.

2. • CommentRowNumber2.
   • CommentAuthorspitters
   • CommentTimeDec 28th 2013
   • PermaLink
   Author: spitters
   Format: MarkdownItexYou may enjoy [this paper](http://www.jstor.org/stable/2589492) on the law of bounded change. Bridges also has a nice book on the topic.

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

3. • CommentRowNumber3.
   • CommentAuthorColin Tan
   • CommentTimeDec 30th 2013
   • PermaLink
   Author: Colin Tan
   Format: TextThank 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.

   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.
4. • CommentRowNumber4.
   • CommentAuthorspitters
   • CommentTimeDec 30th 2013
   • PermaLink
   Author: spitters
   Format: MarkdownItex@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.

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

5. • CommentRowNumber5.
   • CommentAuthorColin Tan
   • CommentTimeDec 30th 2013
   • PermaLink
   Author: Colin Tan
   Format: TextThank you. I will need to read this paper by Bridger and Stolzenberg in detail.

   Thank you. I will need to read this paper by Bridger and Stolzenberg in detail.
6. • CommentRowNumber6.
   • CommentAuthorspitters
   • CommentTimeDec 30th 2013
   • PermaLink
   Author: spitters
   Format: MarkdownItexWe have extended this approach to higher derivatives [here](http://www.logicandanalysis.org/index.php/jla/article/view/174/66). This uses the Hermite-Genocchi formula.

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

7. • CommentRowNumber7.
   • CommentAuthorTobyBartels
   • CommentTimeJan 2nd 2014
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexBTW, 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.

   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.

8. • CommentRowNumber8.
   • CommentAuthorColin Tan
   • CommentTimeJan 20th 2014
   • PermaLink
   Author: Colin Tan
   Format: TextNo problem, Toby. Thanks for answering my question.

   No problem, Toby. Thanks for answering my question.