← Mathematical handbook

Pointwise ordering of normalized clamped-affine copulas

theorem Verification.clamped_prefix_order {a b c d : ℝ} (hbd : b ≤ d) (hm : clampedMean b a = clampedMean d c) (u : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, unitClamp (a - b * ↑t) ≤ ∫ (t : ↑unitInterval) in Set.Iic u, unitClamp (c - d * ↑t)

Equal means and ordered slopes imply the correct order of every lower partial integral.

theorem Verification.diagonalBand_cdf_mono {b d : ℝ} (hb : 0 ≤ b) (hd : 0 ≤ d) (hbd : b ≤ d) (u v : ↑unitInterval) : (diagonalBand b hb).cdf ![u, v] ≤ (diagonalBand d hd).cdf ![u, v]

The family is increasing in the lower-orthant order, including its zero-slope endpoint.