← Mathematical handbook

Polynomial moments of a truncated linear ramp

noncomputable def Verification.ramp (q u : ↑unitInterval) : ℝ

Equations

• Verification.ramp q u = max 0 (↑q - ↑u)

theorem Verification.continuous_ramp (q : ↑unitInterval) : Continuous (ramp q)

theorem Verification.ramp_mem (q u : ↑unitInterval) : ramp q u ∈ Set.Icc 0 1

theorem Verification.integral_ramp_pow (q : ↑unitInterval) (n : ℕ) : ∫ (u : ↑unitInterval), ramp q u ^ (n + 1) = ↑q ^ (n + 2) / (↑n + 2)

theorem Verification.integral_ramp (q : ↑unitInterval) : ∫ (u : ↑unitInterval), ramp q u = ↑q ^ 2 / 2

theorem Verification.integral_ramp_sq (q : ↑unitInterval) : ∫ (u : ↑unitInterval), ramp q u ^ 2 = ↑q ^ 3 / 3

theorem Verification.integral_id_mul_ramp (q : ↑unitInterval) : ∫ (u : ↑unitInterval), ↑u * ramp q u = ↑q ^ 3 / 6

theorem Verification.integral_weight_mul_ramp (q : ↑unitInterval) : ∫ (u : ↑unitInterval), (1 - ↑u) * ramp q u = ↑q ^ 2 / 2 - ↑q ^ 3 / 6

theorem Verification.integral_unit_reflection (f : ↑unitInterval → ℝ) : ∫ (u : ↑unitInterval), f (unitInterval.symm u) = ∫ (u : ↑unitInterval), f u

Reflection preserves the uniform integral on the unit interval.

theorem Verification.integral_complement_reflected_ramp_sq (q : ↑unitInterval) : ∫ (u : ↑unitInterval), (1 - ramp q (unitInterval.symm u)) ^ 2 = 1 - ↑q ^ 2 + ↑q ^ 3 / 3

theorem Verification.integral_weight_complement_reflected_ramp (q : ↑unitInterval) : ∫ (u : ↑unitInterval), (1 - ↑u) * (1 - ramp q (unitInterval.symm u)) = 1 / 2 - ↑q ^ 3 / 6

theorem Verification.integral_unit_two_halves (f g : ℝ → ℝ) (hf : Continuous f) (hg : Continuous g) : (∫ (v : ↑unitInterval), if ↑v ≤ 1 / 2 then f ↑v else g (1 - ↑v)) = ∫ (v : ℝ) in 0..1 / 2, f v + g v

theorem Verification.integral_sqrt_two_cube_half : ∫ (v : ℝ) in 0..1 / 2, √(2 * v) ^ 3 = 1 / 5