theorem
Verification.checkerboardRow_embed_antitone
{n : ℕ}
(C : ProbabilityTheory.Copula 2)
(hC : C.IsSI)
(m : ℕ)
(hm : 0 < m)
(Q : ProbabilityTheory.Copula.IntervalPartition n)
(j : Fin n)
(v : ↑unitInterval)
:
Antitone fun (i : Fin m) =>
checkerboardRow (C.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform m hm) Q) i (partitionEmbed Q j v)
theorem
Verification.checkerboardRow_embed_prefix
{n : ℕ}
(C : ProbabilityTheory.Copula 2)
(m : ℕ)
(hm : 0 < m)
(Q : ProbabilityTheory.Copula.IntervalPartition n)
(j : Fin n)
(v : ↑unitInterval)
(k : Fin (m + 1))
:
(∑ i : Fin m,
if ↑i < ↑k then
checkerboardRow (C.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform m hm) Q) i (partitionEmbed Q j v)
else 0) = ↑m * ((1 - ↑v) * C.cdf ![(ProbabilityTheory.Copula.IntervalPartition.uniform m hm).point k, Q.point j.castSucc] + ↑v * C.cdf ![(ProbabilityTheory.Copula.IntervalPartition.uniform m hm).point k, Q.point j.succ])
theorem
Verification.checkerboardRow_energy_le
{n : ℕ}
(C : ProbabilityTheory.Copula 2)
(hC : C.IsCI)
(m : ℕ)
(hm : 0 < m)
(Q : ProbabilityTheory.Copula.IntervalPartition n)
(j : Fin n)
(v : ↑unitInterval)
:
∑ i : Fin m,
(ProbabilityTheory.Copula.IntervalPartition.uniform m hm).width i * checkerboardRow (C.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform m hm) Q) i
(partitionEmbed Q j v) ^ 2 ≤ ∫ (u : ↑unitInterval), C.conditionalCDF u (partitionEmbed Q j v) ^ 2