← Mathematical handbook

Reflection of the predictor and simultaneous reflection preserve xi

theorem Verification.integral_reflected_Iic (f : ↑unitInterval → ℝ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (u : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, f (unitInterval.symm t) = (∫ (t : ↑unitInterval), f t) - ∫ (t : ↑unitInterval) in Set.Iic (unitInterval.symm u), f t

theorem Verification.conditionalCDF_reflect_first (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (C.reflect {0}).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => C.conditionalCDF (unitInterval.symm u) v

theorem Verification.xi_reflect_first (C : ProbabilityTheory.Copula 2) : (C.reflect {0}).chatterjeeXi = C.chatterjeeXi

theorem Verification.xi_survival (C : ProbabilityTheory.Copula 2) : C.survivalCopula.chatterjeeXi = C.chatterjeeXi