Smooth maps composed with absolutely continuous curves

Locally Lipschitz maps preserve the absolute continuity of metric-valued curves under composition, and isometries moreover reflect it. In particular, a map that is continuously differentiable near every point of the compact trace of an absolutely continuous curve preserves absolute continuity.

theorem LocallyLipschitzOn.comp_absolutelyContinuousOnInterval {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {φ : X → Y} {γ : ℝ → X} {s : Set X} {a b : ℝ} (hφ : LocallyLipschitzOn s φ) (hmap : Set.MapsTo γ (Set.uIcc a b) s) (hγ : AbsolutelyContinuousOnInterval γ a b) : AbsolutelyContinuousOnInterval (φ ∘ γ) a b

A locally Lipschitz map preserves the absolute continuity of a metric-valued curve whose trace lies in its domain of local Lipschitz continuity.

theorem Isometry.absolutelyContinuousOnInterval_comp_iff {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} (hf : Isometry f) {γ : ℝ → X} {a b : ℝ} : AbsolutelyContinuousOnInterval (f ∘ γ) a b ↔ AbsolutelyContinuousOnInterval γ a b

Post-composition with an isometry preserves and reflects the absolute continuity of a metric-valued curve.

theorem AbsolutelyContinuousOnInterval.comp_of_contDiffAt {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {γ : ℝ → F} {φ : F → G} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hφ : ∀ x ∈ γ '' Set.uIcc a b, ContDiffAt ℝ 1 φ x) : AbsolutelyContinuousOnInterval (φ ∘ γ) a b

Composing an absolutely continuous curve with a map that is C¹ at every point of its trace preserves absolute continuity. The smoothness assumption is local to the trace.

theorem AbsolutelyContinuousOnInterval.log {f : ℝ → ℝ} {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (h0 : ∀ t ∈ Set.uIcc a b, f t ≠ 0) : AbsolutelyContinuousOnInterval (fun (t : ℝ) => Real.log (f t)) a b

The logarithm of an absolutely continuous real function that does not vanish on the interval is absolutely continuous.