← Mathematical handbook

Measurability and boundedness of conditional means

theorem Verification.conditionalMean_measurable (C : ProbabilityTheory.Copula 2) : Measurable (conditionalMean C)

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

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