Quasi-every monotone function is strictly increasing

Support module for MiscMath.Analysis.KolmogorovArnold, where the theorem is stated and where the reader should start; Layer 1 of the development, the part that pays for the StrictMono clause of the statement, which none of the five primaries states (Kahane remarks it; Morris, Bull. Amer. Math. Soc. 58 (2021), Theorem 4.2, states it). Its declarations are proof: machine-generated, kernel-checked and axiom-audited, and may be read by no one.

The Baire-category proof produces a tuple of inner functions in the complete metric space of monotone continuous functions on I = [0, 1], and the residual set it produces is stable under intersection with any other dense Gδ. Kahane observed that the strictly increasing functions contain one, so the tuple can be taken strictly increasing at no further cost. This module proves that observation, for one function and for tuples.

What this module proves

In the space Inner of monotone continuous functions I → ℝ with the sup metric:

• for a < b in I, the set of φ with φ(a) < φ(b) is open and dense (isOpen_sepSet, dense_sepSet);
• there is a dense Gδ set G every member of which is strictly increasing (exists_isGδ_dense_strictMono);
• for every n there is a dense Gδ set of 2n + 1-tuples every component of which is strictly increasing (exists_isGδ_dense_strictMono_tuple).

"Dense Gδ" is what "quasi-every" means in Kahane's usage: a countable intersection of dense open sets, hence itself dense by the Baire category theorem since the space is complete.

Source

J.-P. Kahane, Sur le théorème de superposition de Kolmogorov, J. Approx. Theory 13 (1975) 229–234, p. 231: "Quasi toute φ est strictement croissante, car visiblement, pour tout couple de rationnels (ρ, ρ') tels que 0 ≤ ρ < ρ' ≤ 1, l'ensemble des φ qui vérifient φ(ρ + 0) < φ(ρ' − 0) est un ouvert dense dans Φ." His Φ is the space of increasing continuous φ : I → I with φ(0) = 0, φ(1) = 1; here the normalisation is dropped and the functions are real-valued, which changes nothing in the argument. The countable dense set of points is taken abstractly rather than as the rationals, and the intersection is over pairs from it.

Hedberg, The Kolmogorov superposition theorem (LNM 187, 1971), Remark 2, p. 272–273, runs the Baire argument in the closed subspace H of non-decreasing functions but does not take the further step to strictly increasing ones; the theorem's StrictMono rests on Kahane's remark alone, and this module is where that remark is proved.

Sanity checks

The examples below check the two edges of the separating sets: sepSet a a is empty (no function separates a point from itself), and the identity is in sepSet a b for every a < b, so the sets whose intersection is taken are non-empty for exactly the pairs that matter. The main theorems are existence statements with no hypotheses, so there is no satisfiability witness to give; the tuple version is instantiated at n = 2.

Relation to Mathlib

Uses IsGδ.biInter_of_isOpen, dense_biInter_of_isOpen (Baire), dense_pi, IsGδ.preimage, and TopologicalSpace.exists_countable_dense on I. Mathlib has nothing about generic properties of monotone functions in C(I, ℝ).

def MiscMath.Analysis.KolmogorovArnold.sepSet (a b : ↑unitInterval) : Set Inner

The inner functions that strictly separate a from b: φ a < φ b.

Equations

• MiscMath.Analysis.KolmogorovArnold.sepSet a b = {φ : MiscMath.Analysis.KolmogorovArnold.Inner | ↑φ a < ↑φ b}

theorem MiscMath.Analysis.KolmogorovArnold.mem_sepSet {a b : ↑unitInterval} {φ : Inner} : φ ∈ sepSet a b ↔ ↑φ a < ↑φ b

theorem MiscMath.Analysis.KolmogorovArnold.isOpen_sepSet (a b : ↑unitInterval) : IsOpen (sepSet a b)

theorem MiscMath.Analysis.KolmogorovArnold.dense_sepSet {a b : ↑unitInterval} (hab : a < b) : Dense (sepSet a b)

For a < b, the separating set is dense: φ + (r/2) • id is monotone, within r of φ, and separates.

def MiscMath.Analysis.KolmogorovArnold.sepSet' (a b : ↑unitInterval) : Set Inner

The conditional separating set {φ | a < b → φ a < φ b}: the separating set when a < b and everything otherwise. Phrased this way so that it is indexed by all pairs.

Equations

• MiscMath.Analysis.KolmogorovArnold.sepSet' a b = {φ : MiscMath.Analysis.KolmogorovArnold.Inner | a < b → ↑φ a < ↑φ b}

theorem MiscMath.Analysis.KolmogorovArnold.isOpen_sepSet' (a b : ↑unitInterval) : IsOpen (sepSet' a b)

theorem MiscMath.Analysis.KolmogorovArnold.dense_sepSet' (a b : ↑unitInterval) : Dense (sepSet' a b)

def MiscMath.Analysis.KolmogorovArnold.strictGδ (D : Set ↑unitInterval) : Set Inner

Kahane's Gδ: the functions separating every pair a < b drawn from a set D.

Equations

• MiscMath.Analysis.KolmogorovArnold.strictGδ D = ⋂ ab ∈ D ×ˢ D, MiscMath.Analysis.KolmogorovArnold.sepSet' ab.1 ab.2

theorem MiscMath.Analysis.KolmogorovArnold.isGδ_strictGδ {D : Set ↑unitInterval} (hD : D.Countable) : IsGδ (strictGδ D)

theorem MiscMath.Analysis.KolmogorovArnold.dense_strictGδ {D : Set ↑unitInterval} (hD : D.Countable) : Dense (strictGδ D)

theorem MiscMath.Analysis.KolmogorovArnold.exists_mem_Ioo_of_dense {D : Set ↑unitInterval} (hD : Dense D) {x y : ↑unitInterval} (hxy : x < y) : ∃ a ∈ D, x < a ∧ a < y

Between any two points of I there is a point of a dense set.

theorem MiscMath.Analysis.KolmogorovArnold.strictMono_of_mem_strictGδ {D : Set ↑unitInterval} (hD : Dense D) {φ : Inner} (hφ : φ ∈ strictGδ D) : StrictMono ⇑↑φ

A function separating every pair from a dense set is strictly increasing.

theorem MiscMath.Analysis.KolmogorovArnold.exists_isGδ_dense_strictMono : ∃ (G : Set Inner), IsGδ G ∧ Dense G ∧ ∀ φ ∈ G, StrictMono ⇑↑φ

Quasi-every monotone continuous function on I is strictly increasing (Kahane 1975, p. 231): the strictly increasing functions contain a dense Gδ of Inner.

theorem MiscMath.Analysis.KolmogorovArnold.exists_isGδ_dense_strictMono_tuple (n : ℕ) : ∃ (G : Set (InnerTuple n)), IsGδ G ∧ Dense G ∧ ∀ ψ ∈ G, ∀ (q : Fin (2 * n + 1)), StrictMono ⇑↑(ψ q)

Quasi-every tuple of inner functions is strictly increasing in every component: for every n, the tuples all of whose 2n + 1 components are strictly increasing contain a dense Gδ of InnerTuple n.

Sanity checks