← Copula mathematical handbook

Measurability and boundedness of conditional means

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalMean_measurable (C : Copula 2) : Measurable (conditionalMean C)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalMean_mem (C : Copula 2) (u : ↑unitInterval) : conditionalMean C u ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalMean_centered_sq_integrable (C : Copula 2) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => (conditionalMean C u - 1 / 2) ^ 2) MeasureTheory.volume