2
$\begingroup$

When I refer to the Monotone Convergence Theorem below, I refer to the very simple claim that if a non-decreasing sequence has an upper bound then it converges. I don't refer to the claim from Measure Theory.

One application I know of for this theorem is to recurrence relations. One shows that a recurrence relation like $a_{n+1} = \sqrt{2 + a_n}, a_0 = 0$ is non-decreasing and bounded, from which one concludes that it has a limit as $n$ approaches $\infty$.

Are there any other applications of the theorem?

I ask because I'm curious about the possibility of systematically "constructivising" applications of this theorem. Obviously in general this isn't possible. But surely there are lots of situations in which it may be possible.

I tried constructivising Herschfeld's Convergence Theorem, I believe successfully. The resulting argument is a great deal less straightforward than Herschfeld's original one.

[edit]

There was a slight misunderstanding in the comments. The Cauchy completeness of the real numbers does not imply the Monotone Convergence Theorem, unless one assumes the Law of Excluded Middle.

Improve this question
$\endgroup$
20
  • 4
    $\begingroup$ It’s probably one of the most commonly used lemmas in analysis. $\endgroup$
    – Monroe Eskew
    Commented May 2, 2020 at 9:40
  • 1
    $\begingroup$ Yep, that’s what i mean $\endgroup$
    – Monroe Eskew
    Commented May 2, 2020 at 10:00
  • 1
    $\begingroup$ @ogogmad Some experience in analysis would suggest otherwise. This is one of those propositions that's so deep in the background that people use it implicitly. I even used it in a recent work and I'm not really an analyst. Bolzano-Weierstrass is fundamental. Another omnipresently applied result would be Fatou's Lemma in measure theory, which uses the notion of "liminf". The well-definedness of this notion is a manifestation of MCT. $\endgroup$
    – Monroe Eskew
    Commented May 5, 2020 at 8:25
  • 1
    $\begingroup$ @MonroeEskew Thanks for mentioning Fatou's lemma. I'm going to think deeply about this $\endgroup$
    – wlad
    Commented May 5, 2020 at 9:01
  • 1
    $\begingroup$ Well it says that a certain integral is bounded by a certain number defined by liminf. The existence of the number is an implicit claim, no? In any case, it's conceivable that the underlying "ontology" allows things like inequalities to be proven. Maybe a silly example-- Goodstein's Theorem. $\endgroup$
    – Monroe Eskew
    Commented May 5, 2020 at 11:20

2 Answers 2

Reset to default
6
$\begingroup$

I am going to speak in intuitionistic mathematics here, as that's what's relevant for this question.

It's worthwhile recalling a bit of background. There are several notions of completeness of an ordered field:

  • Cauchy completeness: every Cauchy sequence converges.
  • Dedekind completeness: every Dedekind cut determines an element of the field.
  • MacNeille completeness: an inhabited bounded set has a supremum.

The field of rationals may be completeted with respect to any one of these to yield three kinds of reals, the Cauchy reals $\mathbb{R}_C$, the Dedekind reals $\mathbb{R}_D$ and the MacNeille reals $\mathbb{R}_M$. These are related as $\mathbb{R}_C \subset \mathbb{R}_D \subset \mathbb{R}_M$.

The principle "a bounded non-decreasing sequence has a supremum" holds in $\mathbb{R}_M$, but it cannot be shown to hold in $\mathbb{R}_D$ (and even less so in $\mathbb{R}_C$).

The principle does not fail completely for $\mathbb{R}_D$. If $a : \mathbb{N} \to \mathbb{R}_D$ is a non-decreasing sequences, we can define the lower Dedekind cut $L = \{q \in \mathbb{Q} \mid \exists n . q < a_n\}$, but not in general the upper cut. Thus, the supremum $\sup_n a_n$ exists as a lower Dedekind real, which is good enough in some situations.

Many uses of the principle are inessential, especially when with some extra effort we can show that the non-decreasing sequence is Cauchy (I imagine this is what you did to prove Herschfeld's Convergence Theorem). For an essential use, we need to look for applications in which the non-decreasing sequence cannot be shown to be Cauchy. This often happens when the sequence depends on some extra parameters. Let me give one such simple example.

Consider the sequence of functions $f_n : [0,1] \to \mathbb{R}$ where $f_n(x) = x^n$. Using the principle "every bounded non-increasing sequence has an infimum", we can show that $(f_n)_n$ converges point-wise on $[0,1]$. Indeed, given any $x \in [0,1]$, it is easy to see that $x \geq x^2 \geq x^3 \geq \cdots$, therefore $\lim_n f_n(x)$ exists. Of course, the limit map $f(x) = \lim_n x^n$ satisfies $f(1) = 1$ and $f(x) = 0$ for $x \in [0,1)$. Without the principle, we cannot show that $(f_n)_n$ converges pointwise because its limit $f$ would be a discontinuous function.

Incidentally, the above example shows that there are discontinuous maps on MacNeille reals.

Improve this answer
$\endgroup$
11
  • $\begingroup$ Is the sequence $(f_n)_n$ that you defined actually useful in any way? $\endgroup$
    – wlad
    Commented May 2, 2020 at 17:49
  • $\begingroup$ Nice answer otherwise $\endgroup$
    – wlad
    Commented May 2, 2020 at 17:50
  • $\begingroup$ Yes, it demonstrates an essential use of the principle :-). But seriously, once you see this example, you should be able to generate more complex ones by using fancier functions. For example, you can use the principle to show that all sorts of discontinuous functions can be written as Fourier series. $\endgroup$
    – Andrej Bauer
    Commented May 2, 2020 at 17:53
  • 1
    $\begingroup$ I tihnk you're jumping to conclusions. Just because nobody here gave a second and a third application of MCT, that does not mean there isn't one. For instance, wouldn't MCT be useful in measure theory, where we approximate measurable maps from below by sequences of increasing simple maps (you'd have to take piecewise linear, or polynomials)? Another one that comes to mind is a proof that a linear operator $F$ on a Banach space has a norm if it is bounded (in the sense that $\|F x\| \leq M \|x\|$ for some $M > 0$). $\endgroup$
    – Andrej Bauer
    Commented May 5, 2020 at 8:42
  • 1
    $\begingroup$ The Arzela-Ascoli theorem might be another one. There we use the fact that a bounded sequence has a convergent subsequence (as @MonroeEskew pointed out already, that seems to be equivalent to MCT, at least with Dependent choice) in an essential way. The Arzela-Ascoli theorem is used all over the place in analysis (although likely in an inessential way in many concrete cases). $\endgroup$
    – Andrej Bauer
    Commented May 5, 2020 at 8:51
3
$\begingroup$

I'm not sure if this is an answer to your question but it seems like it might be. In enumerative combinatorics one often has a sequence of nonnegative integers $(a_n)$ and wants to estimate its growth rate. A standard way to proceed is to form the generating function $\sum_n a_n x^n$ or $\sum_n a_n x^n\!/n!$ and then show that it converges to an analytic function. Then one can apply methods from complex analysis. The proof of convergence focuses on showing that the sequence $(a_n)$ doesn't grow too fast; one basically takes for granted that this means that the series converges (at least pointwise), because of what you're calling the Monotone Convergence Theorem. There are lots of examples in the book Analytic Combinatorics by Flajolet and Sedgwick.

But I'm not fluent enough with constructive reasoning to tell if this is a trivial or eliminable use of MCT.

Improve this answer
$\endgroup$
3
  • $\begingroup$ In this case, I think you can get away with using the Direct Comparison Test, which can be proved constructively $\endgroup$
    – wlad
    Commented May 2, 2020 at 19:29
  • $\begingroup$ The various convergence tests for infinite series are all constructive. So it seems like it's eliminable $\endgroup$
    – wlad
    Commented May 2, 2020 at 19:30
  • $\begingroup$ Still giving this +1 $\endgroup$
    – wlad
    Commented May 2, 2020 at 19:34

Not the answer you're looking for? Browse other questions tagged .