← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.copulaRowMean_mono {m : ℕ} (P : IntervalPartition m) (C : Copula 2) (i : Fin m) : Monotone (copulaRowMean P C i)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.copulaRowMean_total {m : ℕ} (P : IntervalPartition m) (C : Copula 2) (v : ↑unitInterval) : ∑ i : Fin m, P.width i * copulaRowMean P C i v = ↑v

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.checkerboardRow_interpolation_error {m n : ℕ} (P : IntervalPartition m) (Q : IntervalPartition n) (C : Copula 2) (i : Fin m) (j : Fin n) (v : ↑unitInterval) : |checkerboardRow (C.cellMass P Q) i (partitionEmbed Q j v) - copulaRowMean P C i (partitionEmbed Q j v)| ≤ copulaRowMean P C i (Q.point j.succ) - copulaRowMean P C i (Q.point j.castSucc)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.checkerboard_energy_interpolation_error_embed {m n : ℕ} (P : IntervalPartition m) (Q : IntervalPartition n) (C : Copula 2) (j : Fin n) (v : ↑unitInterval) : |conditionalEnergy (C.cellMass P Q).checkerboard (partitionEmbed Q j v) - rowMeanEnergy P C (partitionEmbed Q j v)| ≤ 2 * Q.width j

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionEmbed_exists {m : ℕ} (P : IntervalPartition m) (v : ↑unitInterval) : ∃ (i : Fin m) (u : ↑unitInterval), partitionEmbed P i u = v

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.checkerboard_energy_interpolation_error {m : ℕ} (P : IntervalPartition m) (C : Copula 2) (n : ℕ) (v : ↑unitInterval) : |conditionalEnergy (C.cellMass P (IntervalPartition.uniform (n + 1) ⋯)).checkerboard v - rowMeanEnergy P C v| ≤ 2 / (↑n + 1)