← Mathematical handbook

Proposition 3.2: all equal-width straight permutation shuffles

The source's positive order N is represented as n+1, with zero-based indices. Thus the source's endpoint conditions π(1)=1 and π(N)=N become π(0)=0 and π(Fin.last n)=Fin.last n. No symmetry assumption is imposed on π.

noncomputable def Papers.Rockel2025Approximation.permutationShuffle (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : ProbabilityTheory.Copula 2

Equations

• Papers.Rockel2025Approximation.permutationShuffle n π = Verification.PermutationShuffle.copula n π

def Papers.Rockel2025Approximation.permutationInversions (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : ℕ

Number of pairs j<i with π(j)>π(i), equivalent to the source's inversion count.

Equations

• Papers.Rockel2025Approximation.permutationInversions n π = Verification.PermutationShuffle.inversions n π

theorem Papers.Rockel2025Approximation.permutationShuffle_cdf (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (u v : ↑unitInterval) : (permutationShuffle n π).cdf ![u, v] = ∑ i : Fin (n + 1), min (Verification.stripCut (1 / (↑n + 1)) (↑↑i / (↑n + 1)) ↑u) (Verification.stripCut (1 / (↑n + 1)) (↑↑(π i) / (↑n + 1)) ↑v)

theorem Papers.Rockel2025Approximation.permutationShuffle_rho (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : (permutationShuffle n π).spearmanRho = 1 - (6 * ∑ i : Fin (n + 1), (↑↑(π i) - ↑↑i) ^ 2) / (↑n + 1) ^ 3

theorem Papers.Rockel2025Approximation.permutationShuffle_tau (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : (permutationShuffle n π).kendallTau = 1 - 4 * ↑(permutationInversions n π) / (↑n + 1) ^ 2

theorem Papers.Rockel2025Approximation.permutationShuffle_xi (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : (permutationShuffle n π).chatterjeeXi = 1

theorem Papers.Rockel2025Approximation.permutationShuffle_lower_tail (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : (permutationShuffle n π).HasLowerTailDependence (if π 0 = 0 then 1 else 0)

theorem Papers.Rockel2025Approximation.permutationShuffle_upper_tail (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : (permutationShuffle n π).HasUpperTailDependence (if π (Fin.last n) = Fin.last n then 1 else 0)