← Mathematical handbook

Integration of a pair of reflected endpoint pieces and a middle piece

theorem Verification.integral_unit_three_pieces {c : ℝ} (hc0 : 0 ≤ c) (hc1 : c ≤ 1 / 2) (f g h : ℝ → ℝ) (hf : Continuous f) (hg : Continuous g) (hh : Continuous h) : (∫ (v : ↑unitInterval), if ↑v ≤ c then f ↑v else if ↑v ≤ 1 - c then g ↑v else h (1 - ↑v)) = (∫ (v : ℝ) in 0..c, f v + h v) + ∫ (v : ℝ) in c..1 - c, g v

theorem Verification.integral_sqrt_scaled_cube {b a : ℝ} (hb : 0 < b) (ha : 0 ≤ a) : ∫ (v : ℝ) in 0..a ^ 2 / (2 * b), √(2 * b * v) ^ 3 = a ^ 5 / (5 * b)

Exact radical integral, using the substitution v=t^2/(2b), including the endpoint.