← Mathematical handbook

Endpoint-safe version of the corrected shuffling path

The author revision flips the upper interval [1-p,1]. Its printed endpoint convention sends both 1-p and 1 to 1-p. This file uses the measure-equivalent convention that flips the closed upper interval, so the map is an exact involution. The two conventions differ only at the split point, which is null under the uniform marginal.

noncomputable def Papers.Rockel2026XiBlest.shuffleCut (p : ↑unitInterval) : ↑unitInterval

Source split point 1-p.

Equations

• Papers.Rockel2026XiBlest.shuffleCut p = ⟨1 - ↑p, ⋯⟩

noncomputable def Papers.Rockel2026XiBlest.printedShuffleReal (p u : ↑unitInterval) : ℝ

The printed piecewise transformation, as a real-valued function.

Equations

• Papers.Rockel2026XiBlest.printedShuffleReal p u = if ↑u ≤ ↑(Papers.Rockel2026XiBlest.shuffleCut p) then ↑u else ↑(Papers.Rockel2026XiBlest.shuffleCut p) + 1 - ↑u

noncomputable def Papers.Rockel2026XiBlest.shuffleReal (p u : ↑unitInterval) : ℝ

An endpoint-safe version that flips the closed upper interval.

Equations

• Papers.Rockel2026XiBlest.shuffleReal p u = if ↑u < ↑(Papers.Rockel2026XiBlest.shuffleCut p) then ↑u else ↑(Papers.Rockel2026XiBlest.shuffleCut p) + 1 - ↑u

theorem Papers.Rockel2026XiBlest.shuffleReal_mem (p u : ↑unitInterval) : shuffleReal p u ∈ Set.Icc 0 1

noncomputable def Papers.Rockel2026XiBlest.shufflePoint (p u : ↑unitInterval) : ↑unitInterval

The endpoint-safe shuffle, interpreted on the unit interval.

Equations

• Papers.Rockel2026XiBlest.shufflePoint p u = ⟨Papers.Rockel2026XiBlest.shuffleReal p u, ⋯⟩

theorem Papers.Rockel2026XiBlest.measurable_shufflePoint (p : ↑unitInterval) : Measurable (shufflePoint p)

theorem Papers.Rockel2026XiBlest.shufflePoint_involution (p u : ↑unitInterval) : shufflePoint p (shufflePoint p u) = u

The endpoint-safe convention is an exact involution.

@[simp]

theorem Papers.Rockel2026XiBlest.shuffleCut_zero : shuffleCut 0 = 1

@[simp]

theorem Papers.Rockel2026XiBlest.shuffleCut_one : shuffleCut 1 = 0

theorem Papers.Rockel2026XiBlest.shufflePoint_zero (u : ↑unitInterval) : shufflePoint 0 u = u

At p=0 the canonical map is exactly the identity.

theorem Papers.Rockel2026XiBlest.shufflePoint_one (u : ↑unitInterval) : shufflePoint 1 u = unitInterval.symm u

At p=1 the canonical map is exactly the coordinate reflection.

theorem Papers.Rockel2026XiBlest.shuffleReal_eq_printed_of_ne (p u : ↑unitInterval) (h : u ≠ shuffleCut p) : shuffleReal p u = printedShuffleReal p u

Except at the split point, the exact involution is the printed map.

theorem Papers.Rockel2026XiBlest.shuffleReal_ae_printed (p : ↑unitInterval) : shuffleReal p =ᵐ[MeasureTheory.volume] printedShuffleReal p

The source and endpoint-safe formulas agree under the uniform law.

theorem Papers.Rockel2026XiBlest.shufflePoint_measurePreserving (p : ↑unitInterval) : MeasureTheory.MeasurePreserving (shufflePoint p) MeasureTheory.volume MeasureTheory.volume

The endpoint-safe upper-interval flip preserves uniform measure.

theorem Papers.Rockel2026XiBlest.copula_measureReal_conditional_set (C : ProbabilityTheory.Copula 2) (s : Set ↑unitInterval) (hs : MeasurableSet s) (v : ↑unitInterval) : C.toMeasure.real {x : Fin 2 → ↑unitInterval | x 0 ∈ s ∧ x 1 ≤ v} = ∫ (u : ↑unitInterval) in s, C.conditionalCDF u v

Disintegration of a copula over any measurable first-coordinate set, extending the usual lower-rectangle conditional-CDF identity.

theorem Papers.Rockel2026XiBlest.shuffle_setIntegral (p : ↑unitInterval) (s : Set ↑unitInterval) (hs : MeasurableSet s) (g : ↑unitInterval → ℝ) (hg : Measurable g) : ∫ (u : ↑unitInterval) in s, g (shufflePoint p u) = ∫ (u : ↑unitInterval) in shufflePoint p ⁻¹' s, g u

Change of variables through the measure-preserving involution.

noncomputable def Papers.Rockel2026XiBlest.shuffleTransform (p : ↑unitInterval) (x : Fin 2 → ↑unitInterval) : Fin 2 → ↑unitInterval

The source transformation applied to the first copula coordinate.

Equations

• Papers.Rockel2026XiBlest.shuffleTransform p x = ![Papers.Rockel2026XiBlest.shufflePoint p (x 0), x 1]

theorem Papers.Rockel2026XiBlest.measurable_shuffleTransform (p : ↑unitInterval) : Measurable (shuffleTransform p)

theorem Papers.Rockel2026XiBlest.shuffleTransform_zero (x : Fin 2 → ↑unitInterval) : shuffleTransform 0 x = x

theorem Papers.Rockel2026XiBlest.shuffleTransform_one (x : Fin 2 → ↑unitInterval) : shuffleTransform 1 x = ProbabilityTheory.Copula.reflectPoint {0} x

noncomputable def Papers.Rockel2026XiBlest.shuffledLaw (C : ProbabilityTheory.Copula 2) (p : ↑unitInterval) : MeasureTheory.Measure (Fin 2 → ↑unitInterval)

Pushforward law along the corrected shuffle, before proving uniformity of its first marginal for every parameter.

Equations

• Papers.Rockel2026XiBlest.shuffledLaw C p = MeasureTheory.Measure.map (Papers.Rockel2026XiBlest.shuffleTransform p) C.toMeasure

theorem Papers.Rockel2026XiBlest.shuffledLaw_zero (C : ProbabilityTheory.Copula 2) : shuffledLaw C 0 = C.toMeasure

theorem Papers.Rockel2026XiBlest.shuffledLaw_one (C : ProbabilityTheory.Copula 2) : shuffledLaw C 1 = (C.reflect {0}).toMeasure

noncomputable def Papers.Rockel2026XiBlest.shuffledCopula (C : ProbabilityTheory.Copula 2) (p : ↑unitInterval) : ProbabilityTheory.Copula 2

Every parameter of the corrected shuffle is a copula: the first marginal stays uniform by the interval-flip theorem, and the second marginal is unchanged. No SI assumption is needed for this construction.

Equations

• Papers.Rockel2026XiBlest.shuffledCopula C p = ProbabilityTheory.Copula.ofMap C.measure (Papers.Rockel2026XiBlest.shuffleTransform p) ⋯ ⋯

theorem Papers.Rockel2026XiBlest.toMeasure_shuffledCopula (C : ProbabilityTheory.Copula 2) (p : ↑unitInterval) : (shuffledCopula C p).toMeasure = shuffledLaw C p

theorem Papers.Rockel2026XiBlest.shuffledCopula_zero (C : ProbabilityTheory.Copula 2) : shuffledCopula C 0 = C

Corrected shuffling lemma (i), initial endpoint.

theorem Papers.Rockel2026XiBlest.shuffledCopula_one (C : ProbabilityTheory.Copula 2) : shuffledCopula C 1 = C.reflect {0}

Corrected shuffling lemma (i), reflected endpoint.

theorem Papers.Rockel2026XiBlest.shuffledCopula_conditionalCDF_ae (C : ProbabilityTheory.Copula 2) (p v : ↑unitInterval) : (fun (u : ↑unitInterval) => (shuffledCopula C p).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => C.conditionalCDF (shufflePoint p u) v

Conditional CDFs of the shuffle are obtained by composing the original conditional CDF with the inverse first-coordinate map.

theorem Papers.Rockel2026XiBlest.shuffle_integral_comp (p : ↑unitInterval) (g : ↑unitInterval → ℝ) : ∫ (u : ↑unitInterval), g (shufflePoint p u) = ∫ (u : ↑unitInterval), g u

Uniform integration is invariant under the exact shuffle.

theorem Papers.Rockel2026XiBlest.shuffledCopula_xi (C : ProbabilityTheory.Copula 2) (p : ↑unitInterval) : (shuffledCopula C p).chatterjeeXi = C.chatterjeeXi

Corrected shuffling lemma (ii): any measurable rearrangement of the conditioning coordinate by this involution preserves directional xi.

theorem Papers.Rockel2026XiBlest.shuffledCopula_cdf_setIntegral (C : ProbabilityTheory.Copula 2) (p u v : ↑unitInterval) : (shuffledCopula C p).cdf ![u, v] = ∫ (t : ↑unitInterval) in shufflePoint p ⁻¹' Set.Iic u, C.conditionalCDF t v

The shuffled CDF is an integral of the original conditional section over the inverse image of its first-coordinate lower interval.

theorem Papers.Rockel2026XiBlest.shuffledCopula_cdf_below_cut (C : ProbabilityTheory.Copula 2) (p u v : ↑unitInterval) (hu : u < shuffleCut p) : (shuffledCopula C p).cdf ![u, v] = C.cdf ![u, v]

Below the split, the shuffle leaves each lower rectangle unchanged.

theorem Papers.Rockel2026XiBlest.shuffledCopula_cdf_above_cut (C : ProbabilityTheory.Copula 2) (p u v r : ↑unitInterval) (hu : shuffleCut p ≤ u) (hr : ↑r = ↑(shuffleCut p) + 1 - ↑u) : (shuffledCopula C p).cdf ![u, v] = C.cdf ![shuffleCut p, v] + ↑v - C.cdf ![r, v]

Above the split, the CDF is the lower unflipped mass plus the upper tail mass reflected from the source copula.

theorem Papers.Rockel2026XiBlest.si_cdf_cross (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) (a b c d v : ↑unitInterval) (hab : a ≤ b) (hbd : b ≤ d) (hac : a ≤ c) (hcd : c ≤ d) (hsum : ↑a + ↑d = ↑b + ↑c) : C.cdf ![a, v] + C.cdf ![d, v] ≤ C.cdf ![b, v] + C.cdf ![c, v]

Equal-length increments of an SI copula's concave CDF section decrease as the interval moves right. The four-point form also covers overlapping intervals.

theorem Papers.Rockel2026XiBlest.shuffledCopula_lowerOrthant (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) (p q : ↑unitInterval) (hpq : q ≤ p) : (shuffledCopula C p).LowerOrthantLE (shuffledCopula C q)

Corrected shuffling lemma (iii): increasing the flipped upper length decreases the copula in lower orthant order.

theorem Papers.Rockel2026XiBlest.shuffledCopula_concordance (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) (p q : ↑unitInterval) (hpq : q ≤ p) : (shuffledCopula C p).ConcordanceLE (shuffledCopula C q)

The same corrected order in the source's concordance convention.

theorem Papers.Rockel2026XiBlest.cdf_first_lipschitz (C : ProbabilityTheory.Copula 2) (a b v : ↑unitInterval) : |C.cdf ![a, v] - C.cdf ![b, v]| ≤ |↑a - ↑b|

A copula CDF is one-Lipschitz in its first coordinate.

theorem Papers.Rockel2026XiBlest.shuffledCopula_cdf_bound_ordered (C : ProbabilityTheory.Copula 2) (p q u v : ↑unitInterval) (hpq : q ≤ p) : |(shuffledCopula C p).cdf ![u, v] - (shuffledCopula C q).cdf ![u, v]| ≤ 2 * (↑p - ↑q)

For ordered parameters, every CDF value changes by at most twice the parameter difference. This does not require SI.

theorem Papers.Rockel2026XiBlest.shuffledCopula_cdf_bound (C : ProbabilityTheory.Copula 2) (p q u v : ↑unitInterval) : |(shuffledCopula C p).cdf ![u, v] - (shuffledCopula C q).cdf ![u, v]| ≤ 2 * |↑p - ↑q|

The uniform CDF bound for arbitrary parameter pairs.

theorem Papers.Rockel2026XiBlest.shuffledCopula_uniformCDF_continuous (C : ProbabilityTheory.Copula 2) (ε : ℝ) : 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ (p q : ↑unitInterval), |↑p - ↑q| < δ → ∀ (x : Fin 2 → ↑unitInterval), |(shuffledCopula C p).cdf x - (shuffledCopula C q).cdf x| < ε

Corrected shuffling lemma (iv), in a quantitative uniform-CDF form. The same parameter modulus works at every point of the closed square.

theorem Papers.Rockel2026XiBlest.shuffleReal_ae_printed_copula (C : ProbabilityTheory.Copula 2) (p : ↑unitInterval) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, ↑(shufflePoint p (x 0)) = printedShuffleReal p (x 0)

The boundary convention used in the source changes no transformed copula law because every copula has a uniform, atomless first marginal.