← Mathematical handbook

Threshold probabilities restricted to a prefix of the unit interval

theorem Verification.integral_prefix_le_real (t : ↑unitInterval) (r : ℝ) : (∫ (u : ↑unitInterval) in Set.Iic t, if ↑u ≤ r then 1 else 0) = min (↑t) (max 0 r)

theorem Verification.integral_prefix_ge_real (t : ↑unitInterval) (r : ℝ) : (∫ (u : ↑unitInterval) in Set.Iic t, if r ≤ ↑u then 1 else 0) = ↑t - min (↑t) (max 0 r)