Substitution by decreasing absolutely continuous parameters

Change of variables holds for antitone absolutely continuous substitutions, including constant pieces and unbounded speeds. Reflecting the parameter interval reduces the results to increasing substitutions. The oriented image interval records the sign reversal.

theorem AbsolutelyContinuousOnInterval.intervalIntegrable_deriv_smul_comp_of_antitoneOn {θ : ℝ → ℝ} {a b : ℝ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → F} (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (hanti : AntitoneOn θ (Set.Icc a b)) (hf : IntervalIntegrable f MeasureTheory.volume (θ a) (θ b)) : IntervalIntegrable (fun (t : ℝ) => deriv θ t • f (θ t)) MeasureTheory.volume a b

An antitone absolutely continuous substitution preserves integrability after multiplication by its derivative.

theorem AbsolutelyContinuousOnInterval.integral_deriv_smul_comp_of_antitoneOn {θ : ℝ → ℝ} {a b : ℝ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → F} (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (hanti : AntitoneOn θ (Set.Icc a b)) (hf : IntervalIntegrable f MeasureTheory.volume (θ a) (θ b)) : ∫ (t : ℝ) in a..b, deriv θ t • f (θ t) = ∫ (u : ℝ) in θ a..θ b, f u

Change of variables for an antitone absolutely continuous substitution and an integrable vector-valued integrand. The decreasing oriented image interval records the sign reversal.