Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
Thanks! nice.
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.
I see that I am repeating myself (from that nforum discussion). Sorry.
No problem. So far, I have only read the first page of that paper. But I have a Jstor password somewhere …
Classically, the MVT (and hence the Law of Bounded Change) does not require uniform differentiabilty on . 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 on (extended by continuity) or ; classically, the MVT applies to these. (Side query: is there an example, say on , that's differentiable with a bounded derivative on but that is not differentiable at ? 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 is unbounded, the derivative of is bounded in absolute value by , so the Law of Bounded Change would tell us that the difference quotients of (on any interval, really) are also bounded in absolute value by . 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 is uniformly continuous on (with ) and ____ly differentiable on with on , then . 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.)
OK, I guess that it's ‘obvious’ that the theorem holds whenever is uniformly differentiable on every closed subinterval of (as long as is also continuous at and ). It would still be nice to have a condition that follows, classically, from pointwise differentiability; there's still the example of on (extended by continuity).
But maybe this is centipede mathematics. After all, the mean-value inequality also applies to things like on . The really general theorem holds whenever there is a finite (isolated) subset of such that is continuous at every point in and (uniformly) differentiable on (every closed subinterval of) the (metric) complement of . (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.
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 , might be continuous at and , might be pointwise differentiable on , and might have a bounded derivative on , but might have a larger difference quotient from to ? Bonus if it might be uniformly continuous on . (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 is nonnegative on and is continuous at and , then . 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 that is continuous at and (or better, uniformly continuous on ), differentiable on with a nonnegative derivative, yet ? I can't even imagine how to start.
1 to 9 of 9