← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionCenter {n : ℕ} (P : IntervalPartition n) (i : Fin n) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionCenter P i = ↑(P.point i.castSucc) + P.width i / 2

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partition_center_mean {n : ℕ} (P : IntervalPartition n) : ∑ i : Fin n, P.width i * partitionCenter P i = 1 / 2

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.cellMass_total {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) : ∑ i : Fin m, ∑ j : Fin n, A.mass i j = 1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.cellMass_first_center {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) : ∑ i : Fin m, ∑ j : Fin n, A.mass i j * partitionCenter P i = 1 / 2

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.cellMass_second_center {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) : ∑ i : Fin m, ∑ j : Fin n, A.mass i j * partitionCenter Q j = 1 / 2