Substitution by absolutely continuous changes of parameter

Absolutely continuous substitutions satisfy change of variables for continuous integrands. For monotone substitutions, the derivative-weighted pushforward of interval volume is interval volume on the image, giving change of variables and transformed integrability for arbitrary integrable normed-space-valued integrands. This accommodates constant pieces and unbounded parameter speeds.

theorem AbsolutelyContinuousOnInterval.integral_comp_mul_deriv_of_continuous {θ : ℝ → ℝ} {a b : ℝ} (hθ : AbsolutelyContinuousOnInterval θ a b) {f : ℝ → ℝ} (hf : Continuous f) : ∫ (t : ℝ) in a..b, f (θ t) * deriv θ t = ∫ (u : ℝ) in θ a..θ b, f u

Substitution of an absolutely continuous function in the integral of a continuous real integrand. The substitution need not be monotone.

theorem AbsolutelyContinuousOnInterval.map_withDensity_deriv_of_monotoneOn {θ : ℝ → ℝ} {a b : ℝ} (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (hmono : MonotoneOn θ (Set.Icc a b)) : MeasureTheory.Measure.map θ ((MeasureTheory.volume.restrict (Set.Icc a b)).withDensity fun (t : ℝ) => ENNReal.ofReal (deriv θ t)) = MeasureTheory.volume.restrict (Set.Icc (θ a) (θ b))

For an increasing absolutely continuous substitution, pushing interval volume weighted by its derivative forward gives ordinary volume on the image interval.

theorem AbsolutelyContinuousOnInterval.integrableOn_deriv_smul_comp_iff_of_monotoneOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → F} {θ : ℝ → ℝ} {a b : ℝ} (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (hmono : MonotoneOn θ (Set.Icc a b)) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Icc (θ a) (θ b)))) : MeasureTheory.IntegrableOn (fun (t : ℝ) => deriv θ t • f (θ t)) (Set.Icc a b) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn f (Set.Icc (θ a) (θ b)) MeasureTheory.volume

Under a monotone absolutely continuous substitution, integrability of the derivative-weighted composition is equivalent to integrability on the image interval.

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

A monotone absolutely continuous substitution preserves integrability after multiplication by its derivative.

theorem AbsolutelyContinuousOnInterval.integral_deriv_smul_comp_of_monotoneOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → F} {θ : ℝ → ℝ} {a b : ℝ} (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (hmono : MonotoneOn θ (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 a monotone absolutely continuous substitution and an integrable vector-valued integrand. Constant pieces and unbounded parameter speeds are allowed.