Absolutely continuous paths

Absolute continuity of the standard real extension of a path is preserved by reversal, concatenation, and truncation. These facts use the existing Path operations.

theorem Path.absolutelyContinuousOnInterval_extend {X : Type u_1} [PseudoMetricSpace X] {x y : X} {γ : Path x y} (hγ : AbsolutelyContinuousOnInterval (⇑γ.extend) 0 1) (a b : ℝ) : AbsolutelyContinuousOnInterval (⇑γ.extend) a b

The constant extension of an absolutely continuous path is absolutely continuous on every real parameter interval.

theorem Path.absolutelyContinuousOnInterval_extend_symm {X : Type u_1} [PseudoMetricSpace X] {x y : X} {γ : Path x y} (hγ : AbsolutelyContinuousOnInterval (⇑γ.extend) 0 1) : AbsolutelyContinuousOnInterval (⇑γ.symm.extend) 0 1

Reversing a path preserves absolute continuity of its standard real extension.

theorem Path.absolutelyContinuousOnInterval_extend_trans {X : Type u_1} [PseudoMetricSpace X] {x y z : X} {γ₁ : Path x y} {γ₂ : Path y z} (h₁ : AbsolutelyContinuousOnInterval (⇑γ₁.extend) 0 1) (h₂ : AbsolutelyContinuousOnInterval (⇑γ₂.extend) 0 1) : AbsolutelyContinuousOnInterval (⇑(γ₁.trans γ₂).extend) 0 1

Concatenating two absolutely continuous paths preserves absolute continuity.

theorem Path.absolutelyContinuousOnInterval_extend_truncate {X : Type u_1} [PseudoMetricSpace X] {x y : X} {γ : Path x y} (hγ : AbsolutelyContinuousOnInterval (⇑γ.extend) 0 1) (t₀ t₁ : ℝ) : AbsolutelyContinuousOnInterval (⇑(γ.truncate t₀ t₁).extend) 0 1

Truncating an absolutely continuous path preserves absolute continuity, with arbitrary real truncation parameters.