Documentation

Papers.OrendayLaresRockel2026XiBeta.IntervalExchange

← Mathematical handbook

The interval exchange `T_b` of Proposition 4.2 #

For b ∈ [-1, 1] put s_b = (1 + b) / 4 ∈ [0, 1/2]. The map T_b : [0,1] → [0,1] swaps the two middle intervals (s_b, 1/2] and (1/2, 1 - s_b] of equal length 1/2 - s_b (by translations) and fixes the two outer ones: T_b(u) = u + 1/2 - s_b for s_b < u ≤ 1/2, u - 1/2 + s_b for 1/2 < u ≤ 1 - s_b, and u otherwise. We work first with a real cut point s ∈ [0, 1/2] and specialize to s = (1 + b) / 4 in intervalExchange.

noncomputable def Papers.OrendayLaresRockel2026XiBeta.xchgReal (s u : ℝ) :

The piecewise translation T on the real line with cut point s.

Equations

Papers.OrendayLaresRockel2026XiBeta.xchgReal s u = if s < u ∧ u ≤ 1 / 2 then u + 1 / 2 - s else if 1 / 2 < u ∧ u ≤ 1 - s then u - 1 / 2 + s else u

Instances For

theorem Papers.OrendayLaresRockel2026XiBeta.xchgReal_mem {s : ℝ} (hs : s ∈ Set.Icc 0 (1 / 2)) {u : ℝ} (hu : u ∈ Set.Icc 0 1) :

xchgReal s u ∈ Set.Icc 0 1

theorem Papers.OrendayLaresRockel2026XiBeta.xchgReal_xchgReal {s : ℝ} (hs : s ∈ Set.Icc 0 (1 / 2)) (u : ℝ) :

xchgReal s (xchgReal s u) = u

theorem Papers.OrendayLaresRockel2026XiBeta.xchgReal_one_sub {s : ℝ} (hs : s ∈ Set.Icc 0 (1 / 2)) {u : ℝ} (h1 : u ≠ s) (h2 : u ≠ 1 / 2) (h3 : u ≠ 1 - s) :

xchgReal s (1 - u) = 1 - xchgReal s u

Reflection equivariance of T away from the three cut points s, 1/2, 1 - s.

theorem Papers.OrendayLaresRockel2026XiBeta.measurable_xchgReal (s : ℝ) :

Measurable (xchgReal s)

noncomputable def Papers.OrendayLaresRockel2026XiBeta.xchg (s : ℝ) (u : ↑unitInterval) :

↑unitInterval

The interval exchange on [0,1] with cut point s (the value is clamped to [0,1], which is inactive for s ∈ [0,1/2], see coe_xchg).

Equations

Papers.OrendayLaresRockel2026XiBeta.xchg s u = Set.projIcc 0 1 Papers.OrendayLaresRockel2026XiBeta.xchg._proof_1 (Papers.OrendayLaresRockel2026XiBeta.xchgReal s ↑u)

Instances For

theorem Papers.OrendayLaresRockel2026XiBeta.coe_xchg {s : ℝ} (hs : s ∈ Set.Icc 0 (1 / 2)) (u : ↑unitInterval) :

↑(xchg s u) = xchgReal s ↑u

theorem Papers.OrendayLaresRockel2026XiBeta.measurable_xchg (s : ℝ) :

Measurable (xchg s)

theorem Papers.OrendayLaresRockel2026XiBeta.xchg_xchg {s : ℝ} (hs : s ∈ Set.Icc 0 (1 / 2)) (u : ↑unitInterval) :

xchg s (xchg s u) = u

theorem Papers.OrendayLaresRockel2026XiBeta.xchg_symm {s : ℝ} (hs : s ∈ Set.Icc 0 (1 / 2)) {u : ↑unitInterval} (h1 : ↑u ≠ s) (h2 : ↑u ≠ 1 / 2) (h3 : ↑u ≠ 1 - s) :

xchg s (unitInterval.symm u) = unitInterval.symm (xchg s u)

noncomputable def Papers.OrendayLaresRockel2026XiBeta.exchangeCut (b : ℝ) :

The cut point s_b = (1 + b) / 4.

Equations

Papers.OrendayLaresRockel2026XiBeta.exchangeCut b = (1 + b) / 4

Instances For

theorem Papers.OrendayLaresRockel2026XiBeta.exchangeCut_mem {b : ℝ} (hb : b ∈ Set.Icc (-1) 1) :

exchangeCut b ∈ Set.Icc 0 (1 / 2)

noncomputable def Papers.OrendayLaresRockel2026XiBeta.intervalExchange (b : ℝ) :

↑unitInterval → ↑unitInterval

The interval exchange T_b of Proposition 4.2.

Equations

Papers.OrendayLaresRockel2026XiBeta.intervalExchange b = Papers.OrendayLaresRockel2026XiBeta.xchg (Papers.OrendayLaresRockel2026XiBeta.exchangeCut b)

Instances For

theorem Papers.OrendayLaresRockel2026XiBeta.coe_intervalExchange {b : ℝ} (hb : b ∈ Set.Icc (-1) 1) (u : ↑unitInterval) :

↑(intervalExchange b u) = if (1 + b) / 4 < ↑u ∧ ↑u ≤ 1 / 2 then ↑u + 1 / 2 - (1 + b) / 4 else if 1 / 2 < ↑u ∧ ↑u ≤ 1 - (1 + b) / 4 then ↑u - 1 / 2 + (1 + b) / 4 else ↑u

The defining formula of T_b.

theorem Papers.OrendayLaresRockel2026XiBeta.ae_coe_ne (c : ℝ) :

∀ᵐ (u : ↑unitInterval), ↑u ≠ c