Staircase functions

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

The approximating inner functions of Hedberg's Lemma 2 (his property a)) are constant on each cell of their rank and vary only across the gaps. Rather than define such a function piecewise, it is written as a finite sum of clamped ramps,

stair q c J u = c 0 + ∑_{j < J} (c (j+1) - c j) · clamp01 (u - (q + m j)),

where clamp01 v = max 0 (min 1 v) and c : ℕ → ℝ is the sequence of levels. Each ramp is 0 up to the right endpoint of cell j and 1 from the left endpoint of cell j + 1, so on cell j (for j ≤ J) the sum telescopes to c j (stair_eq_of_mem_cell), and across the gap after cell j the value moves monotonically from c j to c (j+1) (stair_mem_Icc_of_gap). Continuity and monotonicity (for monotone levels) are each one Mathlib lemma about finite sums of continuous, respectively monotone, functions with non-negative coefficients — the reason for this form over an Int.floor-based case split. stairInner packages t ↦ stair q c J (N t) as an element of the inner-function space Inner.

def MiscMath.Analysis.KolmogorovArnold.clamp01 (v : ℝ) : ℝ

The clamp of a real to [0, 1]: max 0 (min 1 v).

Equations

• MiscMath.Analysis.KolmogorovArnold.clamp01 v = max 0 (min 1 v)

theorem MiscMath.Analysis.KolmogorovArnold.clamp01_of_nonpos {v : ℝ} (h : v ≤ 0) : clamp01 v = 0

theorem MiscMath.Analysis.KolmogorovArnold.clamp01_of_one_le {v : ℝ} (h : 1 ≤ v) : clamp01 v = 1

theorem MiscMath.Analysis.KolmogorovArnold.clamp01_nonneg (v : ℝ) : 0 ≤ clamp01 v

theorem MiscMath.Analysis.KolmogorovArnold.clamp01_le_one (v : ℝ) : clamp01 v ≤ 1

theorem MiscMath.Analysis.KolmogorovArnold.monotone_clamp01 : Monotone clamp01

theorem MiscMath.Analysis.KolmogorovArnold.continuous_clamp01 : Continuous clamp01

def MiscMath.Analysis.KolmogorovArnold.stair {m : ℕ} (q : Fin m) (c : ℕ → ℝ) (J : ℕ) (u : ℝ) : ℝ

The staircase of rank q with levels c and J ramps: constant c j on the cell of index j ≤ J, moving from c j to c (j + 1) across the gap after it.

Equations

• One or more equations did not get rendered due to their size.

theorem MiscMath.Analysis.KolmogorovArnold.continuous_stair {m : ℕ} (q : Fin m) (c : ℕ → ℝ) (J : ℕ) : Continuous (stair q c J)

theorem MiscMath.Analysis.KolmogorovArnold.monotone_stair {m : ℕ} (q : Fin m) {c : ℕ → ℝ} (hc : Monotone c) (J : ℕ) : Monotone (stair q c J)

theorem MiscMath.Analysis.KolmogorovArnold.stair_eq_of_mem_cell {m : ℕ} (q : Fin m) (c : ℕ → ℝ) {J j : ℕ} (hj : j ≤ J) {u : ℝ} (hu : u ∈ cell q j) : stair q c J u = c j

On the cell of index j ≤ J, the staircase takes the value c j.

theorem MiscMath.Analysis.KolmogorovArnold.stair_mem_Icc_of_gap {m : ℕ} (q : Fin m) {c : ℕ → ℝ} (hc : Monotone c) {J j : ℕ} (hj : j + 1 ≤ J) {u : ℝ} (h1 : cellRight q j ≤ u) (h2 : u ≤ cellRight q j + 1) : stair q c J u ∈ Set.Icc (c j) (c (j + 1))

Across the gap after the cell of index j (with j + 1 ≤ J), the staircase lies between c j and c (j + 1).

def MiscMath.Analysis.KolmogorovArnold.stairInner {m : ℕ} (N : ℕ) (q : Fin m) {c : ℕ → ℝ} (hc : Monotone c) (J : ℕ) : Inner

The staircase rescaled to I: t ↦ stair q c J (N t), as an inner function.

Equations

• MiscMath.Analysis.KolmogorovArnold.stairInner N q hc J = ⟨{ toFun := fun (t : ↑unitInterval) => MiscMath.Analysis.KolmogorovArnold.stair q c J (↑N * ↑t), continuous_toFun := ⋯ }, ⋯⟩

@[simp]

theorem MiscMath.Analysis.KolmogorovArnold.stairInner_apply {m : ℕ} (N : ℕ) (q : Fin m) {c : ℕ → ℝ} (hc : Monotone c) (J : ℕ) (t : ↑unitInterval) : ↑(stairInner N q hc J) t = stair q c J (↑N * ↑t)