Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry bundle bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry graph graphs gravity group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homology homotopy homotopy-theory homotopy-type-theory index-theory infinity integration integration-theory itex k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics planar pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorTobyBartels
   • CommentTimeNov 17th 2016
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexUrs had earlier started [[mean value theorem]] with just a link to Wikipedia. I have now added content. Constructive versions to come, hopefully; for now, see [this forum post](https://nforum.ncatlab.org/discussion/5574/constructive-mean-value-theorem/).

   Urs had earlier started mean value theorem with just a link to Wikipedia. I have now added content. Constructive versions to come, hopefully; for now, see this forum post.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeNov 17th 2016
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks! nice.

   Thanks! nice.

3. • CommentRowNumber3.
   • CommentAuthorspitters
   • CommentTimeNov 17th 2016
   • PermaLink
   Author: spitters
   Format: MarkdownItex[Stolzenberg and Bridger](https://www.jstor.org/stable/2589492) argue that in most cases the law of bounded change suffices, and is actually more natural. Together with Coquand, [we showed](http://www.logicandanalysis.org/index.php/jla/article/view/174/66) that this can be used, for instance, to prove Simpson's rule. For this we use divided differences.

   Stolzenberg and Bridger argue that in most cases the law of bounded change suffices, and is actually more natural. Together with Coquand, we showed that this can be used, for instance, to prove Simpson’s rule. For this we use divided differences.

4. • CommentRowNumber4.
   • CommentAuthorspitters
   • CommentTimeNov 17th 2016
   • PermaLink
   Author: spitters
   Format: MarkdownItexI see that I am repeating myself (from that nforum discussion). Sorry.

   I see that I am repeating myself (from that nforum discussion). Sorry.

5. • CommentRowNumber5.
   • CommentAuthorTobyBartels
   • CommentTimeNov 21st 2016
   • (edited Nov 21st 2016)
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexNo problem. So far, I have only read the first page of that paper. But I have a Jstor password somewhere …

   No problem. So far, I have only read the first page of that paper. But I have a Jstor password somewhere …

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeFeb 7th 2020
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexState the mean-value inequality; note its relevance to constructive mathematics and to Lipschitz continuity. <a href="https://ncatlab.org/nlab/revision/diff/mean+value+theorem/6">diff</a>, <a href="https://ncatlab.org/nlab/revision/mean+value+theorem/6">v6</a>, <a href="https://ncatlab.org/nlab/show/mean+value+theorem">current</a>

   State the mean-value inequality; note its relevance to constructive mathematics and to Lipschitz continuity.

   diff, v6, current

7. • CommentRowNumber7.
   • CommentAuthorTobyBartels
   • CommentTimeFeb 11th 2020
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexClassically, the MVT (and hence the Law of Bounded Change) does not require uniform differentiabilty on $[a,b]$. For one thing, uniform differentiability is stronger (even classically) than differentiability (it\'s classically equivalent to differentiability with a uniformly continuous derivative); for another thing, the function does not need to be differentiable at the endpoints (as long as it\'s still continuous there). For examples, consider $f(x) = x^2 \sin(1/x)$ on $[a,b] = [0,1]$ (extended by continuity) or $g(x) = \sqrt{x}$; classically, the MVT applies to these. (Side query: is there an example, say on $[0,1]$, that\'s differentiable with a bounded derivative on $]0,1[$ but that is not differentiable at $0$? That would be the best example, but I haven\'t found one, nor proved that it\'s impossible, even classically.) So the constructive Law of Bounded Change seems substantially weaker. It doesn\'t apply to these examples (even though the classical conclusion holds constructively since they\'re so cleanly defined). Although the derivative of $g$ is unbounded, the derivative of $f$ is bounded in absolute value by $1$, so the Law of Bounded Change would tell us that the difference quotients of $f$ (on any interval, really) are also bounded in absolute value by $1$. Classically, it does tell us this; and constructively, it\'s true. But what is the constructive theorem that guarantees this? I would like to say that if $f$ is uniformly continuous on $[a,b]$ (with $a \lt b$) and ____ly differentiable on $]a,b[$ with $f' \leq M$ on $]a,b[$, then $f(b) - f(a) \leq M (b - a)$. But I don\'t know how to fill in the blank. Is it enough to be uniformly differentiable on compact subintervals? (Both of my examples satisfy that.)

   Classically, the MVT (and hence the Law of Bounded Change) does not require uniform differentiabilty on $[a,b]$. For one thing, uniform differentiability is stronger (even classically) than differentiability (it's classically equivalent to differentiability with a uniformly continuous derivative); for another thing, the function does not need to be differentiable at the endpoints (as long as it's still continuous there). For examples, consider $f(x) = x^2 \sin(1/x)$ on $[a,b] = [0,1]$ (extended by continuity) or $g(x) = \sqrt{x}$; classically, the MVT applies to these. (Side query: is there an example, say on $[0,1]$, that's differentiable with a bounded derivative on $]0,1[$ but that is not differentiable at $0$? That would be the best example, but I haven't found one, nor proved that it's impossible, even classically.)

   So the constructive Law of Bounded Change seems substantially weaker. It doesn't apply to these examples (even though the classical conclusion holds constructively since they're so cleanly defined). Although the derivative of $g$ is unbounded, the derivative of $f$ is bounded in absolute value by $1$, so the Law of Bounded Change would tell us that the difference quotients of $f$ (on any interval, really) are also bounded in absolute value by $1$. Classically, it does tell us this; and constructively, it's true. But what is the constructive theorem that guarantees this?

   I would like to say that if $f$ is uniformly continuous on $[a,b]$ (with $a \lt b$) and ____ly differentiable on $]a,b[$ with $f' \leq M$ on $]a,b[$, then $f(b) - f(a) \leq M (b - a)$. But I don't know how to fill in the blank. Is it enough to be uniformly differentiable on compact subintervals? (Both of my examples satisfy that.)

8. • CommentRowNumber8.
   • CommentAuthorTobyBartels
   • CommentTimeFeb 15th 2020
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexOK, I guess that it's ‘obvious’ that the theorem holds whenever $f$ is uniformly differentiable on every closed subinterval of $]a,b[$ (as long as $f$ is also continuous at $a$ and $b$). It would still be nice to have a condition that follows, classically, from pointwise differentiability; there\'s still the example of $f(x) = x^2 \sin(1/x)$ on $[a,b] = [-1,1]$ (extended by continuity). But maybe this is centipede mathematics. After all, the mean-value inequality also applies to things like $f(x) = {|x|}$ on $[a,b] = [-1,1]$. The really general theorem holds whenever there is a finite (isolated) subset $S$ of $[a,b]$ such that $f$ is continuous at every point in $S$ and (uniformly) differentiable on (every closed subinterval of) the (metric) complement of $S$. (The classical theorem can leave out the stuff in parentheses, while the constructive theorem needs it; furthermore, the stuff in parentheses is classically trivial except for the uniformity of differentiability.) But nobody seems to bother about that level of generality either. There are still functions where the classical mean-value inequality says something but the constructive one doesn\'t, such as [Volterra\'s function](https://en.wikipedia.org/wiki/Volterra%27s_function), which is pointwise differentiable everywhere but uniformly differentiable nowhere. (Well, Volterra\'s function is the derivative, which interested Volterra because it\'s not Riemann-integrable, despite being bounded and having an antiderivative; but the function that we care about is the antiderivative.) But the conclusion is still constructively true for that example.

   OK, I guess that it's ‘obvious’ that the theorem holds whenever $f$ is uniformly differentiable on every closed subinterval of $]a,b[$ (as long as $f$ is also continuous at $a$ and $b$). It would still be nice to have a condition that follows, classically, from pointwise differentiability; there's still the example of $f(x) = x^2 \sin(1/x)$ on $[a,b] = [-1,1]$ (extended by continuity).

   But maybe this is centipede mathematics. After all, the mean-value inequality also applies to things like $f(x) = {|x|}$ on $[a,b] = [-1,1]$. The really general theorem holds whenever there is a finite (isolated) subset $S$ of $[a,b]$ such that $f$ is continuous at every point in $S$ and (uniformly) differentiable on (every closed subinterval of) the (metric) complement of $S$. (The classical theorem can leave out the stuff in parentheses, while the constructive theorem needs it; furthermore, the stuff in parentheses is classically trivial except for the uniformity of differentiability.) But nobody seems to bother about that level of generality either.

   There are still functions where the classical mean-value inequality says something but the constructive one doesn't, such as Volterra's function, which is pointwise differentiable everywhere but uniformly differentiable nowhere. (Well, Volterra's function is the derivative, which interested Volterra because it's not Riemann-integrable, despite being bounded and having an antiderivative; but the function that we care about is the antiderivative.) But the conclusion is still constructively true for that example.

9. • CommentRowNumber9.
   • CommentAuthorTobyBartels
   • CommentTimeFeb 15th 2020
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI\'m also having trouble imagining when the MVI might *not* hold. What is the weak counterexample of a function that might be defined on $[a,b]$, might be continuous at $a$ and $b$, might be pointwise differentiable on $]a,b[$, and might have a bounded derivative on $]a,b[$, but might have a larger difference quotient from $a$ to $b$? Bonus if it might be uniformly continuous on $[a,b]$. (Might because these conditions can't all hold classically, so we can't expect to prove them all constructively, just not refute any of them constructively.) If it\'s easier, take the Rolle\'s Theorem version of the MVI: if $f'$ is nonnegative on $]a,b[$ and $f$ is continuous at $a$ and $b$, then $f(a) \leq f(b)$. So can we find (in the weak sense of constructing something that might exist and might have these properties, as far as can be proved constructively) a function $f$ that is continuous at $a$ and $b$ (or better, uniformly continuous on $[a,b]$), differentiable on $]a,b[$ with a nonnegative derivative, yet $f(a) \gt f(b)$? I can\'t even imagine how to start.

   I'm also having trouble imagining when the MVI might not hold. What is the weak counterexample of a function that might be defined on $[a,b]$, might be continuous at $a$ and $b$, might be pointwise differentiable on $]a,b[$, and might have a bounded derivative on $]a,b[$, but might have a larger difference quotient from $a$ to $b$? Bonus if it might be uniformly continuous on $[a,b]$. (Might because these conditions can't all hold classically, so we can't expect to prove them all constructively, just not refute any of them constructively.)

   If it's easier, take the Rolle's Theorem version of the MVI: if $f'$ is nonnegative on $]a,b[$ and $f$ is continuous at $a$ and $b$, then $f(a) \leq f(b)$. So can we find (in the weak sense of constructing something that might exist and might have these properties, as far as can be proved constructively) a function $f$ that is continuous at $a$ and $b$ (or better, uniformly continuous on $[a,b]$), differentiable on $]a,b[$ with a nonnegative derivative, yet $f(a) \gt f(b)$? I can't even imagine how to start.