← Mathematical handbook

Conditional means and correlation ratio for two-strip copulas

theorem Verification.stripKernel_measurable (g : StripDisplacement) : Measurable fun (p : ↑unitInterval × ↑unitInterval) => stripKernel g p.1 p.2

theorem Verification.conditionalMean_twoStrip (g : StripDisplacement) : conditionalMean (twoStrip g) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => if u ≤ ProbabilityTheory.Copula.unitHalf then 1 / 2 - ∫ (v : ↑unitInterval), g.toFun v else 1 / 2 + ∫ (v : ↑unitInterval), g.toFun v

theorem Verification.correlationRatio_twoStrip (g : StripDisplacement) : correlationRatio (twoStrip g) = 12 * (∫ (v : ↑unitInterval), g.toFun v) ^ 2