← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.checkerboardRow {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (i : Fin m) (v : ↑unitInterval) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.checkerboardRow A i v = ∑ j : Fin n, A.mass i j / P.width i * ↑(Q.coord j v)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.cellMass_row_prefix {m n : ℕ} (C : Copula 2) (P : IntervalPartition m) (Q : IntervalPartition n) (i : Fin m) (k : Fin (n + 1)) : (∑ j : Fin n, if ↑j < ↑k then (C.cellMass P Q).mass i j else 0) = C.cdf ![P.point i.succ, Q.point k] - C.cdf ![P.point i.castSucc, Q.point k]

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.checkerboardRow_grid {m n : ℕ} (C : Copula 2) (P : IntervalPartition m) (Q : IntervalPartition n) (i : Fin m) (k : Fin (n + 1)) : checkerboardRow (C.cellMass P Q) i (Q.point k) = copulaRowMean P C i (Q.point k)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partition_coord_embed_affine {n : ℕ} (Q : IntervalPartition n) (j s : Fin n) (v : ↑unitInterval) : ↑(Q.coord s (partitionEmbed Q j v)) = (1 - ↑v) * ↑(Q.coord s (Q.point j.castSucc)) + ↑v * ↑(Q.coord s (Q.point j.succ))

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.checkerboardRow_embed {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (i : Fin m) (j : Fin n) (v : ↑unitInterval) : checkerboardRow A i (partitionEmbed Q j v) = (1 - ↑v) * checkerboardRow A i (Q.point j.castSucc) + ↑v * checkerboardRow A i (Q.point j.succ)