Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma 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 foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck 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 homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad 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 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 stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTobyBartels
    • CommentTimeNov 17th 2016

    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.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeNov 17th 2016

    Thanks! nice.

    • CommentRowNumber3.
    • CommentAuthorspitters
    • CommentTimeNov 17th 2016

    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.

    • CommentRowNumber4.
    • CommentAuthorspitters
    • CommentTimeNov 17th 2016

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

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeNov 21st 2016
    • (edited Nov 21st 2016)

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

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 7th 2020

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

    diff, v6, current

    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 11th 2020

    Classically, the MVT (and hence the Law of Bounded Change) does not require uniform differentiabilty on [a,b][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 2sin(1/x)f(x) = x^2 \sin(1/x) on [a,b]=[0,1][a,b] = [0,1] (extended by continuity) or g(x)=xg(x) = \sqrt{x}; classically, the MVT applies to these. (Side query: is there an example, say on [0,1][0,1], that's differentiable with a bounded derivative on ]0,1[]0,1[ but that is not differentiable at 00? 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 gg is unbounded, the derivative of ff is bounded in absolute value by 11, so the Law of Bounded Change would tell us that the difference quotients of ff (on any interval, really) are also bounded in absolute value by 11. 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 ff is uniformly continuous on [a,b][a,b] (with a<ba \lt b) and ____ly differentiable on ]a,b[]a,b[ with fMf' \leq M on ]a,b[]a,b[, then f(b)f(a)M(ba)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.)

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 16th 2020

    OK, I guess that it's ‘obvious’ that the theorem holds whenever ff is uniformly differentiable on every closed subinterval of ]a,b[]a,b[ (as long as ff is also continuous at aa and bb). It would still be nice to have a condition that follows, classically, from pointwise differentiability; there's still the example of f(x)=x 2sin(1/x)f(x) = x^2 \sin(1/x) on [a,b]=[1,1][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|f(x) = {|x|} on [a,b]=[1,1][a,b] = [-1,1]. The really general theorem holds whenever there is a finite (isolated) subset SS of [a,b][a,b] such that ff is continuous at every point in SS and (uniformly) differentiable on (every closed subinterval of) the (metric) complement of SS. (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.

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 16th 2020

    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][a,b], might be continuous at aa and bb, might be pointwise differentiable on ]a,b[]a,b[, and might have a bounded derivative on ]a,b[]a,b[, but might have a larger difference quotient from aa to bb? Bonus if it might be uniformly continuous on [a,b][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 ff' is nonnegative on ]a,b[]a,b[ and ff is continuous at aa and bb, then f(a)f(b)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 ff that is continuous at aa and bb (or better, uniformly continuous on [a,b][a,b]), differentiable on ]a,b[]a,b[ with a nonnegative derivative, yet f(a)>f(b)f(a) \gt f(b)? I can't even imagine how to start.