← Mathematical handbook

noncomputable def Verification.orderHalf {n : ℕ} (r i : Fin n) : ℝ

Equations

• Verification.orderHalf r i = if r < i then 1 else if r = i then 1 / 2 else 0

theorem Verification.patchwork_cell_cdf_integral {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (C : Fin m → Fin n → ProbabilityTheory.Copula 2) (i r : Fin m) (j s : Fin n) : ∫ (x : Fin 2 → ↑unitInterval), (C r s).cdf ![P.coord r (partitionEmbed P i (x 0)), Q.coord s (partitionEmbed Q j (x 1))] ∂(C i j).toMeasure = orderHalf r i * orderHalf s j + if r = i ∧ s = j then (C i j).kendallTau / 4 else 0

theorem Verification.patchwork_tau_formula {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (C : Fin m → Fin n → ProbabilityTheory.Copula 2) : (A.patchwork C).kendallTau = 4 * ∑ i : Fin m, ∑ j : Fin n, ∑ r : Fin m, ∑ s : Fin n, A.mass i j * A.mass r s * orderHalf r i * orderHalf s j - 1 + ∑ i : Fin m, ∑ j : Fin n, A.mass i j ^ 2 * (C i j).kendallTau