← Mathematical handbook

Integrating an intercept primitive over a truncated unit-height band

theorem Verification.integral_truncated_primitive {w a : ↑unitInterval → ℝ} (hw : MeasureTheory.Integrable w MeasureTheory.volume) (ha : Monotone a) (hprim : ∀ (v : ↑unitInterval), ∫ (t : ↑unitInterval) in Set.Iic v, w t = a v) (l r : ↑unitInterval) (hlr : l ≤ r) (A : ℝ) (hl : a l = A) (hr : a r = A + 1) (v : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic v, (Set.Ioc l r).indicator w t = unitClamp (a v - A)

Truncating the primitive between levels A and A+1 gives its unit clamp.