← Copula mathematical handbook

Blest's coefficient as a quadratic-weighted conditional CDF integral

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.integral_weighted_lower {g : ↑unitInterval → ℝ} (hg : Measurable g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) : ∫ (u : ↑unitInterval), (1 - ↑u) * ∫ (w : ↑unitInterval) in Set.Iic u, g w = (∫ (w : ↑unitInterval), (1 - ↑w) ^ 2 * g w) / 2

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.integrable_blest_section (C : Copula 2) (v : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => (1 - ↑u) ^ 2 * C.conditionalCDF u v) MeasureTheory.volume

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.blest_conditional_formula (C : Copula 2) : blestNu C = (12 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), (1 - ↑u) ^ 2 * C.conditionalCDF u v) - 2

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.integrable_blest_profile (C : Copula 2) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => ∫ (u : ↑unitInterval), (1 - ↑u) ^ 2 * C.conditionalCDF u v) MeasureTheory.volume