The inner-function space

Support module for MiscMath.Analysis.KolmogorovArnold, where the theorem is stated and where the reader should start; Layer 1 of the development. Its declarations are proof: machine-generated, kernel-checked and axiom-audited, and may be read by no one.

The Baire-category proof of the superposition theorem (Hedberg 1971, Kahane 1975) works in a complete metric space of candidate inner functions and shows that the tuples which work are residual. This module fixes that space:

• monoMaps, the monotone elements of C(I, ℝ), a closed set;
• Inner, that set as a type — Hedberg's H (his Remark 2) and Kahane's Φ without his normalisation φ(0) = 0, φ(1) = 1, which is a proof device we do not need — complete because closed subsets of complete spaces are complete;
• InnerTuple n, the 2n + 1-fold product with the sup metric, which is complete and therefore a Baire space.

Everything past the closedness proof is an instance Mathlib already supplies. Here I is Mathlib's unitInterval, so an inner function is a function on [0, 1]; extending to ℝ is the last layer's business.

def MiscMath.Analysis.KolmogorovArnold.monoMaps : Set C(↑unitInterval, ℝ)

The monotone (non-decreasing) continuous real functions on I, as a set in C(I, ℝ).

Equations

• MiscMath.Analysis.KolmogorovArnold.monoMaps = {φ : C(↑unitInterval, ℝ) | Monotone ⇑φ}

theorem MiscMath.Analysis.KolmogorovArnold.monoMaps_eq_iInter : monoMaps = ⋂ (a : ↑unitInterval), ⋂ (b : ↑unitInterval), ⋂ (_ : a ≤ b), {φ : C(↑unitInterval, ℝ) | φ a ≤ φ b}

monoMaps is the intersection over a ≤ b of the closed conditions φ a ≤ φ b.

theorem MiscMath.Analysis.KolmogorovArnold.isClosed_monoMaps : IsClosed monoMaps

@[reducible, inline]

abbrev MiscMath.Analysis.KolmogorovArnold.Inner : Type

The inner-function space H: monotone continuous functions I → ℝ with the sup metric.

Equations

• MiscMath.Analysis.KolmogorovArnold.Inner = ↑MiscMath.Analysis.KolmogorovArnold.monoMaps

instance MiscMath.Analysis.KolmogorovArnold.instCompleteSpaceInner : CompleteSpace Inner

@[reducible, inline]

abbrev MiscMath.Analysis.KolmogorovArnold.InnerTuple (n : ℕ) : Type

The space of 2n + 1-tuples of inner functions, with the sup metric.

Equations

• MiscMath.Analysis.KolmogorovArnold.InnerTuple n = (Fin (2 * n + 1) → MiscMath.Analysis.KolmogorovArnold.Inner)

theorem MiscMath.Analysis.KolmogorovArnold.Inner.monotone (φ : Inner) : Monotone ⇑↑φ

An inner function is monotone.

theorem MiscMath.Analysis.KolmogorovArnold.Inner.continuous (φ : Inner) : Continuous ⇑↑φ

An inner function is continuous.

def MiscMath.Analysis.KolmogorovArnold.Inner.id : Inner

The identity t ↦ t as an inner function.

Equations

• MiscMath.Analysis.KolmogorovArnold.Inner.id = ⟨{ toFun := Subtype.val, continuous_toFun := MiscMath.Analysis.KolmogorovArnold.Inner.id._proof_1 }, ⋯⟩

@[simp]

theorem MiscMath.Analysis.KolmogorovArnold.Inner.coe_id_apply (t : ↑unitInterval) : ↑id t = ↑t

instance MiscMath.Analysis.KolmogorovArnold.Inner.instNonempty : Nonempty Inner

def MiscMath.Analysis.KolmogorovArnold.Inner.addSmulId (φ : Inner) (c : ℝ) (hc : 0 ≤ c) : Inner

Adding a non-negative multiple of the identity to an inner function.

Equations

• φ.addSmulId c hc = ⟨↑φ + c • ↑MiscMath.Analysis.KolmogorovArnold.Inner.id, ⋯⟩

@[simp]

theorem MiscMath.Analysis.KolmogorovArnold.Inner.addSmulId_apply (φ : Inner) (c : ℝ) (hc : 0 ≤ c) (t : ↑unitInterval) : ↑(φ.addSmulId c hc) t = ↑φ t + c * ↑t

theorem MiscMath.Analysis.KolmogorovArnold.Inner.dist_addSmulId_le (φ : Inner) (c : ℝ) (hc : 0 ≤ c) : dist (φ.addSmulId c hc) φ ≤ c

The perturbation φ + c • id is within |c| of φ.