← Mathematical handbook

First moments and affine centered-square moments of conditional means

theorem Verification.conditionalMean_integrable (C : ProbabilityTheory.Copula 2) : MeasureTheory.Integrable (conditionalMean C) MeasureTheory.volume

theorem Verification.conditionalMean_integral (C : ProbabilityTheory.Copula 2) : ∫ (u : ↑unitInterval), conditionalMean C u = 1 / 2

theorem Verification.conditionalMean_centered_integral (C : ProbabilityTheory.Copula 2) : ∫ (u : ↑unitInterval), conditionalMean C u - 1 / 2 = 0

theorem Verification.conditionalMean_affine_square_integrable (C : ProbabilityTheory.Copula 2) (r s : ℝ) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => (r * (conditionalMean C u - 1 / 2) + s) ^ 2) MeasureTheory.volume

theorem Verification.conditionalMean_affine_square_integral (C : ProbabilityTheory.Copula 2) (r s : ℝ) : ∫ (u : ↑unitInterval), (r * (conditionalMean C u - 1 / 2) + s) ^ 2 = (r ^ 2 * ∫ (u : ↑unitInterval), (conditionalMean C u - 1 / 2) ^ 2) + s ^ 2