nForum - Discussion Feed (Constructive Mean Value Theorem) 2021-01-16T22:46:56-05:00 https://nforum.ncatlab.org/ Lussumo Vanilla & Feed Publisher Colin Tan comments on "Constructive Mean Value Theorem" (44640) https://nforum.ncatlab.org/discussion/5574/?Focus=44640#Comment_44640 2014-01-20T07:16:20-05:00 2021-01-16T22:46:55-05:00 Colin Tan https://nforum.ncatlab.org/account/199/ No problem, Toby. Thanks for answering my question. No problem, Toby. Thanks for answering my question. ]]> TobyBartels comments on "Constructive Mean Value Theorem" (44262) https://nforum.ncatlab.org/discussion/5574/?Focus=44262#Comment_44262 2014-01-02T00:07:48-05:00 2021-01-16T22:46:55-05:00 TobyBartels https://nforum.ncatlab.org/account/7/ 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.

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.

]]>
spitters comments on "Constructive Mean Value Theorem" (44245) https://nforum.ncatlab.org/discussion/5574/?Focus=44245#Comment_44245 2013-12-30T19:25:22-05:00 2021-01-16T22:46:55-05:00 spitters https://nforum.ncatlab.org/account/936/ We have extended this approach to higher derivatives here. This uses the Hermite-Genocchi formula.

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

]]>
Colin Tan comments on "Constructive Mean Value Theorem" (44235) https://nforum.ncatlab.org/discussion/5574/?Focus=44235#Comment_44235 2013-12-30T13:06:33-05:00 2021-01-16T22:46:55-05:00 Colin Tan https://nforum.ncatlab.org/account/199/ Thank 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. ]]> spitters comments on "Constructive Mean Value Theorem" (44234) https://nforum.ncatlab.org/discussion/5574/?Focus=44234#Comment_44234 2013-12-30T12:12:01-05:00 2021-01-16T22:46:56-05:00 spitters https://nforum.ncatlab.org/account/936/ @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.

]]>
Colin Tan comments on "Constructive Mean Value Theorem" (44231) https://nforum.ncatlab.org/discussion/5574/?Focus=44231#Comment_44231 2013-12-30T08:02:43-05:00 2021-01-16T22:46:56-05:00 Colin Tan https://nforum.ncatlab.org/account/199/ 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 ... 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. ]]> spitters comments on "Constructive Mean Value Theorem" (44220) https://nforum.ncatlab.org/discussion/5574/?Focus=44220#Comment_44220 2013-12-28T21:27:49-05:00 2021-01-16T22:46:56-05:00 spitters https://nforum.ncatlab.org/account/936/ You may enjoy this paper 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.

]]>
TobyBartels comments on "Constructive Mean Value Theorem" (44218) https://nforum.ncatlab.org/discussion/5574/?Focus=44218#Comment_44218 2013-12-28T18:38:57-05:00 2021-01-16T22:46:56-05:00 TobyBartels https://nforum.ncatlab.org/account/7/ I was asked by email whether it is constructively provable that f&prime;=0f' = 0 implies that ff is locally constant. (This is not the Mean Value Theorem, but that's related, and it came up.) ...

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.

]]>