← Mathematical handbook

noncomputable def Verification.rankCellMass (n : ℕ) (hn : 0 < n) (rx ry : Equiv.Perm (Fin n)) : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform n hn) (ProbabilityTheory.Copula.IntervalPartition.uniform n hn)

Fine empirical checkerboard from two rank permutations. Ranks are zero based.

Equations

• Verification.rankCellMass n hn rx ry = { mass := fun (i j : Fin n) => if ry ((Equiv.symm rx) i) = j then 1 / ↑n else 0, nonneg := ⋯, row_sum := ⋯, col_sum := ⋯ }

noncomputable def Verification.rankCopula (n : ℕ) (hn : 0 < n) (rx ry : Equiv.Perm (Fin n)) : ProbabilityTheory.Copula 2

Equations

• Verification.rankCopula n hn rx ry = (Verification.rankCellMass n hn rx ry).checkerboard

theorem Verification.rankCopula_cdf (n : ℕ) (hn : 0 < n) (rx ry : Equiv.Perm (Fin n)) (u v : ↑unitInterval) : (rankCopula n hn rx ry).cdf ![u, v] = 1 / ↑n * ∑ k : Fin n, ↑((ProbabilityTheory.Copula.IntervalPartition.uniform n hn).coord (rx k) u) * ↑((ProbabilityTheory.Copula.IntervalPartition.uniform n hn).coord (ry k) v)