← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partition_coord_embed_self {n : ℕ} (P : IntervalPartition n) (i : Fin n) (u : ↑unitInterval) : P.coord i (partitionEmbed P i u) = u

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partition_coord_embed {n : ℕ} (P : IntervalPartition n) (i r : Fin n) (u : ↑unitInterval) : P.coord r (partitionEmbed P i u) = if r < i then 1 else if r = i then u else 0