← Mathematical handbook

Reflected centered blocks and absolute moments

theorem Verification.integral_centeredOrdinal (C : ProbabilityTheory.Copula 2) (α : ↑unitInterval) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂(centeredOrdinal C α).toMeasure = (↑(centralMargin α) * ∫ (u : ↑unitInterval), f fun (x : Fin 2) => ProbabilityTheory.Copula.OrdinalSum.lowerEmbed (centralMargin α) u) + ↑α * ∫ (x : Fin 2 → ↑unitInterval), f fun (i : Fin 2) => centralEmbed α (x i) ∂C.toMeasure + ↑(centralMargin α) * ∫ (u : ↑unitInterval), f fun (x : Fin 2) => ProbabilityTheory.Copula.OrdinalSum.upperEmbed (centralMargin α) (ProbabilityTheory.Copula.OrdinalSum.upperEmbed (centralSplit α) u)

theorem Verification.centeredOrdinal_abs_sum (C : ProbabilityTheory.Copula 2) (α : ↑unitInterval) : ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) + ↑(x 1) - 1| ∂(centeredOrdinal C α).toMeasure = (1 - ↑α ^ 2) / 2 + ↑α ^ 2 * ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) + ↑(x 1) - 1| ∂C.toMeasure

theorem Verification.footrule_reflect_eq_abs_sum (C : ProbabilityTheory.Copula 2) : (C.reflect {1}).spearmanFootrule = 1 - 3 * ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) + ↑(x 1) - 1| ∂C.toMeasure

theorem Verification.centeredOrdinal_reflect_footrule (C : ProbabilityTheory.Copula 2) (α : ↑unitInterval) : ((centeredOrdinal C α).reflect {1}).spearmanFootrule = ↑α ^ 2 * (C.reflect {1}).spearmanFootrule - (1 - ↑α ^ 2) / 2