9
$\begingroup$

In the replies of this very similar question, there is a fascinating answer that is beautiful in its simplicity. In particular, it seems to use perhaps the most minimal assumptions one can possibly take to prove the approximate intermediate value theorem when the function is only known to be pointwise continuous.

I've perused the web a bit for references on if there is anything similar for the approximate mean value theorem. The discussions I've been able to find seem to be concerned more with the constancy principle, but nonetheless provide some insight into the situation: It seems that one way is assuming "uniform differentiability", at which point standard arguments like that of Bishop or this paper work. Another form of this proof is one where you suppose the fan theorem, at which point you can pass from the pointwise to the uniform. But, to me, this undermines the punch of the aforementioned proof of the approximate intermediate value theorem—why not suppose uniform continuity and do it like Bishop in the same way?

The question that I'm thinking about is this: What is the weakest constructive circumstance under which the approximate mean value theorem holds? Does the derivative need to be pointwise continuous? Do we need some kind of choice or compactness? Or is presupposing uniform differentiability truly the weakest we can go?

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ Well, to start with, in “pure constructive mathematics” (I'm not sure what exactly you mean by that, but I assume something like IZF or the internal logic of a topos, so without even Countable Choice), there is no reason for Cauchy reals and Dedekind reals to be the same (and even “Cauchy reals” can mean several different things, I can think of at least three), so the answer to your question probably depends on exactly what sort of real numbers you want to talk about. $\endgroup$
    – Gro-Tsen
    Commented Nov 5, 2023 at 22:18
  • 1
    $\begingroup$ @Gro-Tsen This was meant to be follow up to Mike Shulman's question (In fact, I thought it to be uncannily similar to it as a question, but there weren't any I could find on this specific topic), and the proof that was given to it in particular. I believe Dedekind reals would be the most optimal, as they seem to be the most concise and useable in a choiceless "least amount of assumptions" sort of environment. So one may approximate any real arbitrarily well with a single rational, but there might not be a Cauchy sequence of such rationals for said real. $\endgroup$
    – SpectreDNZ
    Commented Nov 6, 2023 at 10:21
  • $\begingroup$ In this regard also, I believe anything used for equivalence classes of Cauchy sequences could be translated into something about the Dedekind reals with countable choice, so I'd just take such a proof as saying that we at least need countable choice. Any proof using the Bishop setoid construction, as Mike himself pointed out in the comments of an answer, would be a proof about Cauchy sequences rather than about real numbers. And as Andrej Bauer has repeatedly given as a sentiment, attempting to Cauchy complete the rationals using Cauchy sequences without choice is too arduous a task. $\endgroup$
    – SpectreDNZ
    Commented Nov 6, 2023 at 10:28
  • $\begingroup$ I can't predict to what extent it helps you with your question, but I found this Phd thesis (Schuster, 2013) to be a nice resource, as well as this constructive reverse math text (Diener, 2020). The IVT in the context of different axioms plays a role in both. $\endgroup$
    – Nikolaj-K
    Commented Nov 18, 2023 at 18:00

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .