Reparametrizing integrals of 1-forms along absolutely continuous curves

An absolutely continuous change of parameter that is monotone or antitone preserves the integral of a 1-form along an absolutely continuous curve. Integrability on the original interval implies integrability on the new interval. The oriented image interval records reversal of orientation. The statements use the raw-curve integral ∫ t in a..b, ω (γ t) (deriv γ t). For a Path, Mathlib's curveIntegral_eq_intervalIntegral_deriv gives this representation. The 1-form needs only the integrability of its pairing with the original velocity.

theorem AbsolutelyContinuousOnInterval.intervalIntegrable_oneForm_comp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : ℝ → E} {θ : ℝ → ℝ} {a b : ℝ} {ω : E → E →L[ℝ] F} (hγ : AbsolutelyContinuousOnInterval γ (θ a) (θ b)) (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (horder : MonotoneOn θ (Set.Icc a b) ∨ AntitoneOn θ (Set.Icc a b)) (hω : IntervalIntegrable (fun (t : ℝ) => (ω (γ t)) (deriv γ t)) MeasureTheory.volume (θ a) (θ b)) : IntervalIntegrable (fun (t : ℝ) => (ω ((γ ∘ θ) t)) (deriv (γ ∘ θ) t)) MeasureTheory.volume a b

The integrability of a 1-form paired with an absolutely continuous curve's velocity is preserved by monotone or antitone absolutely continuous changes of parameter.

theorem AbsolutelyContinuousOnInterval.integral_oneForm_comp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : ℝ → E} {θ : ℝ → ℝ} {a b : ℝ} {ω : E → E →L[ℝ] F} (hγ : AbsolutelyContinuousOnInterval γ (θ a) (θ b)) (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (horder : MonotoneOn θ (Set.Icc a b) ∨ AntitoneOn θ (Set.Icc a b)) (hω : IntervalIntegrable (fun (t : ℝ) => (ω (γ t)) (deriv γ t)) MeasureTheory.volume (θ a) (θ b)) : ∫ (t : ℝ) in a..b, (ω ((γ ∘ θ) t)) (deriv (γ ∘ θ) t) = ∫ (u : ℝ) in θ a..θ b, (ω (γ u)) (deriv γ u)

A monotone or antitone absolutely continuous change of parameter preserves the integral of the raw integral ∫ t in a..b, ω (γ t) (deriv γ t), with its oriented image interval.