← Mathematical handbook

Convexity and boundary witnesses for the lower semilinear class

theorem Verification.IsLowerSemilinear.mix {C E : ProbabilityTheory.Copula 2} (hC : IsLowerSemilinear C) (hE : IsLowerSemilinear E) (a : ↑unitInterval) : IsLowerSemilinear (C.mix E a)

The standard lower semilinear class is closed under copula mixtures.

theorem Papers.Rockel2026XiFootrule.upperBoundary_isLowerSemilinear (a : ↑unitInterval) : Verification.IsLowerSemilinear (upperBoundary a)

Every Frechet upper-boundary witness is lower semilinear.

theorem Papers.Rockel2026XiFootrule.diagonalBoundary_isLowerSemilinear (a : ↑unitInterval) : Verification.IsLowerSemilinear (diagonalBoundary a)

Every diagonal lower-boundary witness is lower semilinear.