Total variation and the metric speed of absolutely continuous curves

The total variation of an absolutely continuous metric-valued curve equals the integral of its metric derivative. For curves in finite-dimensional real normed spaces this identifies total variation with the integral of the norm of the canonical derivative.

theorem eVariationOn.le_lintegral_of_edist_le_lintegral {X : Type u_1} [PseudoEMetricSpace X] {γ : ℝ → X} {m : ℝ → ENNReal} {a b : ℝ} (h : ∀ s ∈ Set.Icc a b, ∀ u ∈ Set.Icc a b, edist (γ s) (γ u) ≤ ∫⁻ (t : ℝ) in Set.uIoc s u, m t) : eVariationOn γ (Set.Icc a b) ≤ ∫⁻ (t : ℝ) in Set.Ioc a b, m t

An integral density that controls distances along a curve also controls its total variation.

theorem AbsolutelyContinuousOnInterval.eVariationOn_le_lintegral_metricDerivative {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : eVariationOn γ (Set.uIcc a b) ≤ ∫⁻ (t : ℝ) in Set.uIoc a b, TauCeti.metricDerivative γ t

The integrated metric derivative of an absolutely continuous curve bounds its total variation from above.

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

The cumulative total variation of an absolutely continuous metric-valued curve is an absolutely continuous real function.

theorem AbsolutelyContinuousOnInterval.eVariationOn_eq_lintegral_metricDerivative {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : eVariationOn γ (Set.uIcc a b) = ∫⁻ (t : ℝ) in Set.uIoc a b, TauCeti.metricDerivative γ t

Total variation of an absolutely continuous metric-valued curve is its integrated metric speed, for either orientation of the parameter interval.

theorem AbsolutelyContinuousOnInterval.eVariationOn_eq_lintegral_enorm_deriv {a b : ℝ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} (hγ : AbsolutelyContinuousOnInterval γ a b) : eVariationOn γ (Set.uIcc a b) = ∫⁻ (t : ℝ) in Set.uIoc a b, ‖deriv γ t‖ₑ

In a finite-dimensional real normed space, the total variation of an absolutely continuous curve equals the integral of the norm of its canonical derivative.

theorem AbsolutelyContinuousOnInterval.integral_norm_deriv_eq_eVariationOn_toReal {a b : ℝ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} (hγ : AbsolutelyContinuousOnInterval γ a b) (hab : a ≤ b) : ∫ (t : ℝ) in a..b, ‖deriv γ t‖ = (eVariationOn γ (Set.uIcc a b)).toReal

The real integrated speed of an absolutely continuous finite-dimensional curve is its total variation converted to ℝ, on a nonnegative oriented parameter interval.