Reflection of the response coordinate preserves directional xi #
theorem
ProbabilityTheory.Copula.RankRegion.Common.conditionalCDF_reflect_second
(C : Copula 2)
(v : ↑unitInterval)
:
(fun (u : ↑unitInterval) => (C.reflect {1}).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) =>
1 - C.conditionalCDF u (unitInterval.symm v)