← Mathematical handbook

theorem Verification.uniform_rowMean_antitone (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) (m : ℕ) (hm : 0 < m) (v : ↑unitInterval) : Antitone fun (i : Fin m) => copulaRowMean (ProbabilityTheory.Copula.IntervalPartition.uniform m hm) C i v

theorem Verification.cdf_embed_concavity {n : ℕ} (C : ProbabilityTheory.Copula 2) (hC : C.transpose.IsSI) (Q : ProbabilityTheory.Copula.IntervalPartition n) (j : Fin n) (u v : ↑unitInterval) : (1 - ↑v) * C.cdf ![u, Q.point j.castSucc] + ↑v * C.cdf ![u, Q.point j.succ] ≤ C.cdf ![u, partitionEmbed Q j v]

theorem Verification.uniform_rowMean_prefix (C : ProbabilityTheory.Copula 2) (m : ℕ) (hm : 0 < m) (k : Fin (m + 1)) (v : ↑unitInterval) : (∑ i : Fin m, if ↑i < ↑k then copulaRowMean (ProbabilityTheory.Copula.IntervalPartition.uniform m hm) C i v else 0) = ↑m * C.cdf ![(ProbabilityTheory.Copula.IntervalPartition.uniform m hm).point k, v]