← Mathematical handbook

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

Equations

• Verification.partitionCenter P i = ↑(P.point i.castSucc) + P.width i / 2

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

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

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

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