← Mathematical handbook

Exact marginal means of scaled clamped affine sections

theorem Verification.unitClamp_positive_parts (x : ℝ) : unitClamp x = max 0 x - max 0 (x - 1)

theorem Verification.unitClamp_complement (x : ℝ) : unitClamp (1 - x) = 1 - unitClamp x

theorem Verification.integral_positive_ramp {b a : ℝ} (hb : 0 < b) (ha : 0 ≤ a) (hab : a ≤ b) : ∫ (u : ↑unitInterval), max 0 (a - b * ↑u) = a ^ 2 / (2 * b)

theorem Verification.clampedMean_lower {b a : ℝ} (hb : 0 < b) (ha : 0 ≤ a) (hab : a ≤ b) (ha1 : a ≤ 1) : clampedMean b a = a ^ 2 / (2 * b)

theorem Verification.clampedMean_affine {b a : ℝ} (hb : 0 ≤ b) (hba : b ≤ a) (ha1 : a ≤ 1) : clampedMean b a = a - b / 2

theorem Verification.clampedMean_saturated {b a : ℝ} (hb : 0 < b) (ha1 : 1 ≤ a) (hab : a ≤ b) : clampedMean b a = (a - 1 / 2) / b

theorem Verification.clampedMean_complement (b a : ℝ) : clampedMean b (b + 1 - a) = 1 - clampedMean b a