← Mathematical handbook

Evaluating the clamped-section CDF, including its boundary correction

theorem Verification.integral_prefix_positive_ramp {b : ℝ} (hb : 0 < b) (a : ℝ) (u : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, max 0 (a - b * ↑t) = (max 0 a ^ 2 - max 0 (a - b * ↑u) ^ 2) / (2 * b)

theorem Verification.integral_prefix_clamp {b : ℝ} (hb : 0 < b) (a : ℝ) (u : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, unitClamp (a - b * ↑t) = (max 0 a ^ 2 - max 0 (a - b * ↑u) ^ 2 - max 0 (a - 1) ^ 2 + max 0 (a - 1 - b * ↑u) ^ 2) / (2 * b)