← Copula 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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.PermutationShuffle.strip (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (i : Fin (n + 1)) : ShuffleStrip

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.PermutationShuffle.tile (n : ℕ) (u : ↑unitInterval) : ∑ i : Fin (n + 1), stripCut (1 / (↑n + 1)) (↑↑i / (↑n + 1)) ↑u = ↑u

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.PermutationShuffle.shuffle (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : PositiveShuffle (n + 1)

Equations

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

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

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.PermutationShuffle.copula n π = (ProbabilityTheory.Copula.RankRegion.XiBlest.Support.PermutationShuffle.shuffle n π).copula

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.PermutationShuffle.measurable_graphMap (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : Measurable (graphMap n π)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.PermutationShuffle.functional (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : HasFunctionalWitness (copula n π)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.PermutationShuffle.xi (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : (copula n π).chatterjeeXi = 1

def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.PermutationShuffle.inversions (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : ℕ

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

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.PermutationShuffle.inversions n π = ∑ i : Fin (n + 1), {j : Fin (n + 1) | j < i ∧ π i < π j}.card

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

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.PermutationShuffle.lower_tail (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : (copula n π).HasLowerTailDependence (if π 0 = 0 then 1 else 0)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.PermutationShuffle.upper_tail (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : (copula n π).HasUpperTailDependence (if π (Fin.last n) = Fin.last n then 1 else 0)