← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.orderHalf {n : ℕ} (r i : Fin n) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.orderHalf r i = if r < i then 1 else if r = i then 1 / 2 else 0

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchwork_cell_cdf_integral {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (C : Fin m → Fin n → 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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchwork_tau_formula {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → 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