Extending inner functions from [0, 1] to ℝ

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

The Baire-category argument produces inner functions on I = [0, 1]; the theorem is stated with inner functions continuous and strictly increasing on all of ℝ. The extension used is

Inner.extend φ t = φ (clamp t) + (t - clamp t),

where clamp is Mathlib's Set.projIcc 0 1. It agrees with φ on I (extend_of_mem), is continuous (continuous_extend), and is strictly increasing whenever φ is (extend_strictMono): off I the second term increases strictly, and on I the first does.

noncomputable def MiscMath.Analysis.KolmogorovArnold.Inner.extend (φ : Inner) (t : ℝ) : ℝ

The extension of an inner function from I to ℝ: ψ(clamp t) + (t - clamp t). It agrees with ψ on I, is continuous, and is strictly increasing whenever ψ is: off I the second term increases strictly, and on I the first does.

Equations

• φ.extend t = ↑φ (Set.projIcc 0 1 MiscMath.Analysis.KolmogorovArnold.Inner.extend._proof_1 t) + (t - ↑(Set.projIcc 0 1 MiscMath.Analysis.KolmogorovArnold.Inner.extend._proof_1 t))

theorem MiscMath.Analysis.KolmogorovArnold.Inner.extend_of_mem (φ : Inner) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : φ.extend t = ↑φ ⟨t, ht⟩

theorem MiscMath.Analysis.KolmogorovArnold.Inner.continuous_extend (φ : Inner) : Continuous φ.extend

theorem MiscMath.Analysis.KolmogorovArnold.Inner.extend_strictMono (φ : Inner) (hφ : StrictMono ⇑↑φ) : StrictMono φ.extend