← Mathematical handbook

noncomputable def Verification.cellOverlap {m n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin m) (j : Fin n) : ℝ

Lebesgue overlap of two half-open cells, with the paper's Ico convention.

Equations

• Verification.cellOverlap P Q i j = MeasureTheory.volume.real (Set.Ico (P.point i.castSucc) (P.point i.succ) ∩ Set.Ico (Q.point j.castSucc) (Q.point j.succ))

theorem Verification.cellOverlap_formula {m n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin m) (j : Fin n) : cellOverlap P Q i j = Q.width j * (↑(Q.coord j (P.point i.succ)) - ↑(Q.coord j (P.point i.castSucc)))

theorem Verification.rankCopula_cellMass {m r n : ℕ} (hn : 0 < n) (rx ry : Equiv.Perm (Fin n)) (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition r) (i : Fin m) (j : Fin r) : ((rankCopula n hn rx ry).cellMass P Q).mass i j = ↑n * ∑ k : Fin n, cellOverlap P (ProbabilityTheory.Copula.IntervalPartition.uniform n hn) i (rx k) * cellOverlap Q (ProbabilityTheory.Copula.IntervalPartition.uniform n hn) j (ry k)

Exact fractional rank-binning matrix in the paper, for arbitrary coarse partitions.