Absolutely continuous monotone changes of parameter

Composing an absolutely continuous metric-valued curve with an absolutely continuous monotone change of parameter preserves absolute continuity. Monotonicity is required only on the parameter interval, and the change of parameter may have constant pieces or unbounded speed.

theorem AbsolutelyContinuousOnInterval.comp_monotoneOn {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {θ : ℝ → ℝ} {a b c d : ℝ} (hγ : AbsolutelyContinuousOnInterval γ c d) (hθ_ac : AbsolutelyContinuousOnInterval θ a b) (hθ : MonotoneOn θ (Set.uIcc a b)) (hmap : Set.MapsTo θ (Set.uIcc a b) (Set.uIcc c d)) : AbsolutelyContinuousOnInterval (γ ∘ θ) a b

Absolutely continuous metric-valued curves remain absolutely continuous under an absolutely continuous change of parameter that is monotone on its parameter interval. Constant pieces and unbounded speeds are allowed.

theorem AbsolutelyContinuousOnInterval.comp_antitoneOn {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {θ : ℝ → ℝ} {a b c d : ℝ} (hγ : AbsolutelyContinuousOnInterval γ c d) (hθ_ac : AbsolutelyContinuousOnInterval θ a b) (hθ : AntitoneOn θ (Set.uIcc a b)) (hmap : Set.MapsTo θ (Set.uIcc a b) (Set.uIcc c d)) : AbsolutelyContinuousOnInterval (γ ∘ θ) a b

Absolutely continuous metric-valued curves remain absolutely continuous under an absolutely continuous change of parameter that is antitone on its parameter interval.

theorem AbsolutelyContinuousOnInterval.comp_affine {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b c d : ℝ} (hγ : AbsolutelyContinuousOnInterval γ c d) (m k : ℝ) (hmap : Set.MapsTo (fun (t : ℝ) => m * t + k) (Set.uIcc a b) (Set.uIcc c d)) : AbsolutelyContinuousOnInterval (γ ∘ fun (t : ℝ) => m * t + k) a b

Composing an absolutely continuous metric-valued curve with an affine change of parameter preserves absolute continuity whenever that parameter maps into the curve's interval. The slope may be positive, zero, or negative.

theorem AbsolutelyContinuousOnInterval.comp_lineMap {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : AbsolutelyContinuousOnInterval (γ ∘ ⇑(AffineMap.lineMap a b)) 0 1

Affine normalization to the unit interval preserves absolute continuity for metric-valued curves, including reversed and constant parameter intervals.