← Copula mathematical handbook

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

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

Equations

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

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

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.rankCopula n hn rx ry = (ProbabilityTheory.Copula.RankRegion.XiBlest.Support.rankCellMass n hn rx ry).checkerboard

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.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, ↑((IntervalPartition.uniform n hn).coord (rx k) u) * ↑((IntervalPartition.uniform n hn).coord (ry k) v)