← Mathematical handbook

Identification with the paper's five-piece measure-preserving graph map

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.fivePieceMapReal (d u : ℝ) : ℝ

The five cases of Example 3.10, with exactly the source's endpoint convention.

Equations

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

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.fivePieceMap (d : ℝ) (hd : d ∈ Set.Icc 0 (1 / 2)) (u : ↑unitInterval) : ↑unitInterval

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.fivePieceMap d hd u = ⟨Papers.AnsariRockelSteinmassl2026RhoGamma.fivePieceMapReal d ↑u, ⋯⟩

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_shuffle_graph {s : ℝ} (hs : 1 ≤ s) : have A := ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.halfShift s hs; ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂A.copula.toMeasure, ↑(x 1) = fivePieceMapReal (A.z / 2) ↑(x 0)

The five-segment support identifies the source's graph map almost everywhere.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_shuffle_law {s : ℝ} (hs : 1 ≤ s) (hd : (ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.halfShift s hs).z / 2 ∈ Set.Icc 0 (1 / 2)) : let A := ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.halfShift s hs; A.copula.toMeasure = MeasureTheory.Measure.map (fun (u : ↑unitInterval) => ![u, fivePieceMap (A.z / 2) hd u]) MeasureTheory.volume

Example 3.10: equality of probability measures with the uniform graph construction.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_shuffle_measurePreserving {s : ℝ} (hs : 1 ≤ s) (hd : (ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.halfShift s hs).z / 2 ∈ Set.Icc 0 (1 / 2)) : MeasureTheory.MeasurePreserving (fivePieceMap ((ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.halfShift s hs).z / 2) hd) MeasureTheory.volume MeasureTheory.volume

The exact piecewise map preserves the uniform law.