← Mathematical handbook

The shuffle representation of D_b and measure preservation of T_b

The interval exchange T_b is a four-strip increasing shuffle. Using the library's PositiveShuffle (zero-width strips allowed, so no case split at b = ±1), we build the copula S_b supported on the graph of T_b; from this we deduce that T_b is measure preserving and define D_b as the copula of (U, T_b(U)), i.e. the pushforward of Lebesgue measure under u ↦ (u, T_b u).

noncomputable def Papers.OrendayLaresRockel2026XiBeta.exchangeStrips {s : ℝ} (hs : s ∈ Set.Icc 0 (1 / 2)) : Fin 4 → ProbabilityTheory.Copula.RankRegion.XiBlest.Support.ShuffleStrip

The four strips of the shuffle representing the graph of T with cut point s.

Equations

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

noncomputable def Papers.OrendayLaresRockel2026XiBeta.exchangeShuffle {s : ℝ} (hs : s ∈ Set.Icc 0 (1 / 2)) : ProbabilityTheory.Copula.RankRegion.XiBlest.Support.PositiveShuffle 4

Equations

• Papers.OrendayLaresRockel2026XiBeta.exchangeShuffle hs = { strip := Papers.OrendayLaresRockel2026XiBeta.exchangeStrips hs, total := ⋯, tile_x := ⋯, tile_y := ⋯ }

noncomputable def Papers.OrendayLaresRockel2026XiBeta.exchangeShuffleCopula {s : ℝ} (hs : s ∈ Set.Icc 0 (1 / 2)) : ProbabilityTheory.Copula 2

The copula of the shuffle with the four strips of T (cut point s).

Equations

• Papers.OrendayLaresRockel2026XiBeta.exchangeShuffleCopula hs = (Papers.OrendayLaresRockel2026XiBeta.exchangeShuffle hs).copula

theorem Papers.OrendayLaresRockel2026XiBeta.strip_ae_graph_of {s : ℝ} (hs : s ∈ Set.Icc 0 (1 / 2)) (S : ProbabilityTheory.Copula.RankRegion.XiBlest.Support.ShuffleStrip) (h : 0 < S.width → ∀ (z : ↑unitInterval), z ≠ 0 → S.y + S.width * ↑z = xchgReal s (S.x + S.width * ↑z)) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂S.law, x 1 = xchg s (x 0)

theorem Papers.OrendayLaresRockel2026XiBeta.exchangeShuffle_ae_graph {s : ℝ} (hs : s ∈ Set.Icc 0 (1 / 2)) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂(exchangeShuffleCopula hs).toMeasure, x 1 = xchg s (x 0)

theorem Papers.OrendayLaresRockel2026XiBeta.measurable_graph {f : ↑unitInterval → ↑unitInterval} (hf : Measurable f) : Measurable fun (u : ↑unitInterval) => ![u, f u]

theorem Papers.OrendayLaresRockel2026XiBeta.toMeasure_eq_map_graph (C : ProbabilityTheory.Copula 2) {f : ↑unitInterval → ↑unitInterval} (hf : Measurable f) (h : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, x 1 = f (x 0)) : C.toMeasure = MeasureTheory.Measure.map (fun (u : ↑unitInterval) => ![u, f u]) MeasureTheory.volume

A copula supported a.e. on the graph of a measurable f is the law of (U, f U).

theorem Papers.OrendayLaresRockel2026XiBeta.xchg_measurePreserving {s : ℝ} (hs : s ∈ Set.Icc 0 (1 / 2)) : MeasureTheory.MeasurePreserving (xchg s) MeasureTheory.volume MeasureTheory.volume

theorem Papers.OrendayLaresRockel2026XiBeta.intervalExchange_measurePreserving {b : ℝ} (hb : b ∈ Set.Icc (-1) 1) : MeasureTheory.MeasurePreserving (intervalExchange b) MeasureTheory.volume MeasureTheory.volume

noncomputable def Papers.OrendayLaresRockel2026XiBeta.dExchange (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ProbabilityTheory.Copula 2

The copula D_b of (U, T_b(U)) with U ~ U(0,1).

Equations

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

theorem Papers.OrendayLaresRockel2026XiBeta.toMeasure_dExchange (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (dExchange b hb).toMeasure = MeasureTheory.Measure.map (fun (u : ↑unitInterval) => ![u, intervalExchange b u]) MeasureTheory.volume

theorem Papers.OrendayLaresRockel2026XiBeta.dExchange_eq_shuffle (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : dExchange b hb = exchangeShuffleCopula ⋯