Absolutely continuous curves in pseudometric spaces

Mathlib defines AbsolutelyContinuousOnInterval f a b for maps f : ℝ → X into an arbitrary pseudometric space, but states continuity (AbsolutelyContinuousOnInterval.continuousOn) and bounded variation (AbsolutelyContinuousOnInterval.boundedVariationOn) only for maps into a seminormed additive group. This file supplies both for an arbitrary pseudometric target, as needed for curves in metric spaces which are not normed, such as spaces of probability measures with a Wasserstein distance.

Both are transferred from the normed case along the Fréchet–Kuratowski embedding TauCeti.kuratowskiEmbedding of a pseudometric space into the bounded continuous real functions on it. This embedding is an isometry, so it preserves absolute continuity, continuity and variation.

Main results

• AbsolutelyContinuousOnInterval.continuousOn': an absolutely continuous curve in a pseudometric space is continuous on its interval.
• AbsolutelyContinuousOnInterval.boundedVariationOn': an absolutely continuous curve in a pseudometric space has bounded variation on its interval.
• AbsolutelyContinuousOnInterval.prodMk: a pair of absolutely continuous curves is an absolutely continuous curve in the product.

theorem AbsolutelyContinuousOnInterval.continuousOn' {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : ContinuousOn γ (Set.uIcc a b)

An absolutely continuous curve in a pseudometric space is continuous on its interval. This generalizes AbsolutelyContinuousOnInterval.continuousOn from seminormed groups to pseudometric spaces.

theorem AbsolutelyContinuousOnInterval.boundedVariationOn' {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : BoundedVariationOn γ (Set.uIcc a b)

An absolutely continuous curve in a pseudometric space has bounded variation on its interval. This generalizes AbsolutelyContinuousOnInterval.boundedVariationOn from seminormed groups to pseudometric spaces.

theorem AbsolutelyContinuousOnInterval.prodMk {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} {Y : Type u_2} [PseudoMetricSpace Y] {δ : ℝ → Y} (hγ : AbsolutelyContinuousOnInterval γ a b) (hδ : AbsolutelyContinuousOnInterval δ a b) : AbsolutelyContinuousOnInterval (fun (t : ℝ) => (γ t, δ t)) a b

A pair of absolutely continuous curves in pseudometric spaces is an absolutely continuous curve in their product.