← Mathematical handbook

Equal-width permutation shuffles

The parameter n denotes n+1 strips. Every permutation is allowed, including the one-strip case. The construction uses uniform laws on the actual segments.

theorem Verification.PositiveShuffle.rho {n : ℕ} (S : PositiveShuffle n) : S.copula.spearmanRho = 1 - 6 * ∑ i : Fin n, (S.strip i).width * ((S.strip i).x - (S.strip i).y) ^ 2

noncomputable def Verification.PermutationShuffle.strip (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (i : Fin (n + 1)) : ShuffleStrip

Equations

• Verification.PermutationShuffle.strip n π i = { x := ↑↑i / (↑n + 1), y := ↑↑(π i) / (↑n + 1), width := 1 / (↑n + 1), x_nonneg := ⋯, y_nonneg := ⋯, width_nonneg := ⋯, x_end := ⋯, y_end := ⋯ }

theorem Verification.PermutationShuffle.tile (n : ℕ) (u : ↑unitInterval) : ∑ i : Fin (n + 1), stripCut (1 / (↑n + 1)) (↑↑i / (↑n + 1)) ↑u = ↑u

noncomputable def Verification.PermutationShuffle.shuffle (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : PositiveShuffle (n + 1)

Equations

• Verification.PermutationShuffle.shuffle n π = { strip := Verification.PermutationShuffle.strip n π, total := ⋯, tile_x := ⋯, tile_y := ⋯ }

noncomputable def Verification.PermutationShuffle.copula (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : ProbabilityTheory.Copula 2

Equations

• Verification.PermutationShuffle.copula n π = (Verification.PermutationShuffle.shuffle n π).copula

theorem Verification.PermutationShuffle.ordered_x (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (i j : Fin (n + 1)) (h : i < j) : ((shuffle n π).strip i).x + ((shuffle n π).strip i).width ≤ ((shuffle n π).strip j).x

theorem Verification.PermutationShuffle.ordered_y (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (i j : Fin (n + 1)) (h : π i < π j) : ((shuffle n π).strip i).y + ((shuffle n π).strip i).width ≤ ((shuffle n π).strip j).y

theorem Verification.PermutationShuffle.rho (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : (copula n π).spearmanRho = 1 - (6 * ∑ i : Fin (n + 1), (↑↑(π i) - ↑↑i) ^ 2) / (↑n + 1) ^ 3

noncomputable def Verification.PermutationShuffle.graphMap (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (u : ↑unitInterval) : ↑unitInterval

Equations

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

theorem Verification.PermutationShuffle.measurable_graphMap (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : Measurable (graphMap n π)

theorem Verification.PermutationShuffle.graphMap_point (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (i : Fin (n + 1)) (u : ↑unitInterval) (hu0 : 0 < u) (hu1 : u < 1) : graphMap n π ((strip n π i).point u 0) = (strip n π i).point u 1

theorem Verification.PermutationShuffle.functional (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : HasFunctionalWitness (copula n π)

theorem Verification.PermutationShuffle.xi (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : (copula n π).chatterjeeXi = 1

def Verification.PermutationShuffle.inversions (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : ℕ

Number of inverted pairs, using zero-based strip indices.

Equations

• Verification.PermutationShuffle.inversions n π = ∑ i : Fin (n + 1), {j : Fin (n + 1) | j < i ∧ π i < π j}.card

theorem Verification.PermutationShuffle.tau (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : (copula n π).kendallTau = 1 - 4 * ↑(inversions n π) / (↑n + 1) ^ 2

theorem Verification.PermutationShuffle.diagonal_lower (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (t : ↑unitInterval) (ht : ↑t ≤ 1 / (↑n + 1)) : (copula n π).diagonal t = if π 0 = 0 then ↑t else 0

theorem Verification.PermutationShuffle.diagonal_upper (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (t : ↑unitInterval) (ht : ↑t ≤ 1 / (↑n + 1)) : (copula n π).diagonal (unitInterval.symm t) = 1 - 2 * ↑t + if π (Fin.last n) = Fin.last n then ↑t else 0

theorem Verification.PermutationShuffle.lower_tail (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : (copula n π).HasLowerTailDependence (if π 0 = 0 then 1 else 0)

theorem Verification.PermutationShuffle.upper_tail (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : (copula n π).HasUpperTailDependence (if π (Fin.last n) = Fin.last n then 1 else 0)