×

Lipschitz functions in constructive reverse mathematics. (English) Zbl 1277.03062

In this paper, different formulations of Lipschitz continuity (of functions with compact domain) are studied from the perspective of constructive reverse mathematics.
Recall that in constructive mathematics the usual definition of continuous functions on a compact domain automatically assume uniform continuity. (This goes back to Bishop.)
This paper belongs to a series of papers where one breaks with this custom and studies functions that are defined to be, a priori, pointwise continuous and what logical principles are needed to get uniform continuity; see [H. Diener and the author, J. Log. Anal. 3, Article 8, 26 p. (2011; Zbl 1291.03115)] for previous work.
Here, in particular, the property of Lipschitz continuity is studied. There are statements that a locally Lipschitz continuous function \(f\) is uniformly Lipschitz for
(1) \(f: 2^\mathbb{N} \to \mathbb{R}\),
(2) \(f: [0,1] \to \mathbb{R}\) and with a continuous modulus of Lipschitz continuity,
(3) \(f: 2^\mathbb{N} \to \mathbb{N}\).
It is show that the case (1) follows from the fan theorem for \(\Pi^0_1\)-bars, the case (2) follows from the uniform continuity theorem and with this also from this fan theorem, and (3) follows from the fan theorem for continuous bars.

MSC:

03F60 Constructive and recursive analysis
03B30 Foundations of classical theories (including reverse mathematics)
26A16 Lipschitz (Hölder) classes

Citations:

Zbl 1291.03115
PDFBibTeX XMLCite
Full Text: DOI