← Mathematical handbook

Quantitative uniform bounds for normalized clamped bands

theorem Verification.clamped_deviation {a b : ℝ} (hb : 0 ≤ b) (u : ↑unitInterval) : |unitClamp (a - b * ↑u) - clampedMean b a| ≤ b

Every clamped section is within its slope of its prescribed mean.

theorem Verification.diagonalBand_independence_error (b : ℝ) (hb : 0 ≤ b) (u v : ↑unitInterval) : |(diagonalBand b hb).cdf ![u, v] - ↑u * ↑v| ≤ b

A uniform rate at the independence endpoint.

theorem Verification.diagonalBand_comonotonic_error (b : ℝ) (hb : 0 < b) (u v : ↑unitInterval) : |(diagonalBand b ⋯).cdf ![u, v] - min ↑u ↑v| ≤ 1 / b

A uniform rate at the comonotonic endpoint.