Limits of total variation bounds

This file transfers eventual upper bounds on the total variations of a family of maps to a liminf bound on the total variation of a pointwise limit. It also computes the variation of a composition with an antitone map on an interval, proves stability of bounded variation under addition and subtraction, shows that the variation is unchanged by postcomposition with a map that preserves the distances between the values of the function, and proves bounded variation of constant extensions from closed intervals. Total variation on continuous maps is lower semicontinuous for the compact-open topology, allowing measurable path-space applications.

Main results

• ContinuousMap.lowerSemicontinuous_eVariationOn: lower semicontinuity on continuous path space.
• TauCeti.eVariationOn_le_liminf_of_eventually_le: an eventual bound on the total variations of a family of maps bounds the total variation of a pointwise limit by the liminf of the bounds.
• eVariationOn.comp_inter_Icc_eq_of_antitoneOn: the antitone counterpart of Mathlib's eVariationOn.comp_inter_Icc_eq_of_monotoneOn.
• eVariationOn.comp_eq_of_edist_eq: postcomposition with a map preserving the distances between the values of a function does not change its variation.
• BoundedVariationOn.IccExtend: constant extension from a closed interval preserves bounded variation.
• TauCeti.eVariationOn_id_unitInterval and LipschitzWith.eVariationOn_unitInterval_le: the identity of the unit interval has total variation 1, so a C-Lipschitz map on the unit interval has total variation at most C.

theorem ContinuousMap.lowerSemicontinuous_eVariationOn {α : Type u_1} {E : Type u_2} [LinearOrder α] [TopologicalSpace α] [PseudoEMetricSpace E] (s : Set α) : LowerSemicontinuous fun (f : C(α, E)) => eVariationOn (⇑f) s

Total variation is lower semicontinuous on continuous paths with the compact-open topology. The variation is allowed to be infinite.

@[simp]

theorem TauCeti.eVariationOn_subtypeVal_comp {α : Type u_1} [LinearOrder α] {X : Type u_2} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {s : Set X} {f : α → ↑s} {t : Set α} : eVariationOn f t = eVariationOn (Subtype.val ∘ f) t

The metric variation of a path in a subtype is unchanged by applying its coercion.

theorem TauCeti.eVariationOn_le_liminf_of_eventually_le {α : Type u_1} [LinearOrder α] {X : Type u_2} [PseudoEMetricSpace X] {ι : Type u_3} {l : Filter ι} {s : Set α} {f : α → X} {F : ι → α → X} {u : ι → ENNReal} (hu : ∀ᶠ (i : ι) in l, eVariationOn (F i) s ≤ u i) (hf : ∀ x ∈ s, Filter.Tendsto (fun (i : ι) => F i x) l (nhds (f x))) : eVariationOn f s ≤ Filter.liminf u l

If the total variations of the maps F i on s are eventually bounded by u i, then the total variation on s of a pointwise limit of the F i is at most liminf u.

@[simp]

theorem TauCeti.eVariationOn_subtypeVal_unitInterval : eVariationOn Subtype.val Set.univ = 1

The inclusion of the unit interval into ℝ has total variation 1. This is the simp-normal form of TauCeti.eVariationOn_id_unitInterval.

theorem TauCeti.eVariationOn_id_unitInterval : eVariationOn id Set.univ = 1

The identity of the unit interval has total variation 1.

theorem LipschitzWith.eVariationOn_unitInterval_le {X : Type u_1} [PseudoEMetricSpace X] {f : ↑unitInterval → X} {C : NNReal} (hf : LipschitzWith C f) : eVariationOn f Set.univ ≤ ↑C

A C-Lipschitz map on the unit interval has total variation at most C.

theorem eVariationOn.comp_eq_of_edist_eq {α : Type u_1} {E : Type u_3} [LinearOrder α] [TopologicalSpace E] [WeakPseudoEMetricSpace E] {F : Type u_4} [TopologicalSpace F] [WeakPseudoEMetricSpace F] {f : α → E} {g : E → F} {s : Set α} (h : ∀ x ∈ s, ∀ y ∈ s, edist (g (f x)) (g (f y)) = edist (f x) (f y)) : eVariationOn (g ∘ f) s = eVariationOn f s

Postcomposing f with a map g that preserves the distances between the values of f on s does not change the variation of f on s.

theorem eVariationOn.comp_inter_Icc_eq_of_antitoneOn {α : Type u_1} {β : Type u_2} {E : Type u_3} [LinearOrder α] [LinearOrder β] [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {t : Set β} (φ : β → α) (hφ : AntitoneOn φ t) {x y : β} (hx : x ∈ t) (hy : y ∈ t) : eVariationOn (f ∘ φ) (t ∩ Set.Icc x y) = eVariationOn f (φ '' t ∩ Set.Icc (φ y) (φ x))

The variation of f ∘ φ on t ∩ [x, y] for an antitone φ is the variation of f on the corresponding reversed interval of φ '' t.

theorem BoundedVariationOn.IccExtend {α : Type u_1} {E : Type u_2} [LinearOrder α] [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {a b : α} (hf : BoundedVariationOn f (Set.Icc a b)) (hab : a ≤ b) : BoundedVariationOn (Set.IccExtend hab (f ∘ Subtype.val)) Set.univ

Constant extension of a path outside a closed interval preserves bounded variation.

theorem BoundedVariationOn.congr {α : Type u_1} {E : Type u_2} [LinearOrder α] [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f g : α → E} {s : Set α} (hf : BoundedVariationOn f s) (h : Set.EqOn f g s) : BoundedVariationOn g s

Bounded variation is preserved when functions agree on the domain.

theorem LocallyBoundedVariationOn.congr {α : Type u_1} {E : Type u_2} [LinearOrder α] [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f g : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) (h : Set.EqOn f g s) : LocallyBoundedVariationOn g s

Local bounded variation is preserved when functions agree on the domain.

theorem eVariationOn.add_le {α : Type u_1} {E : Type u_2} [LinearOrder α] [SeminormedAddCommGroup E] {f g : α → E} {s : Set α} : eVariationOn (f + g) s ≤ eVariationOn f s + eVariationOn g s

The variation of a sum is at most the sum of the variations.

@[simp]

theorem eVariationOn.neg {α : Type u_1} {E : Type u_2} [LinearOrder α] [SeminormedAddCommGroup E] {f : α → E} {s : Set α} : eVariationOn (-f) s = eVariationOn f s

Negation does not change the variation of a function.

theorem eVariationOn.sub_le {α : Type u_1} {E : Type u_2} [LinearOrder α] [SeminormedAddCommGroup E] {f g : α → E} {s : Set α} : eVariationOn (f - g) s ≤ eVariationOn f s + eVariationOn g s

The variation of a difference is at most the sum of the variations.

theorem BoundedVariationOn.add {α : Type u_1} {E : Type u_2} [LinearOrder α] [SeminormedAddCommGroup E] {f g : α → E} {s : Set α} (hf : BoundedVariationOn f s) (hg : BoundedVariationOn g s) : BoundedVariationOn (f + g) s

The sum of two bounded-variation functions has bounded variation.

theorem LocallyBoundedVariationOn.add {α : Type u_1} {E : Type u_2} [LinearOrder α] [SeminormedAddCommGroup E] {f g : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) (hg : LocallyBoundedVariationOn g s) : LocallyBoundedVariationOn (f + g) s

Local bounded variation is stable under addition.

theorem BoundedVariationOn.sub {α : Type u_1} {E : Type u_2} [LinearOrder α] [SeminormedAddCommGroup E] {f g : α → E} {s : Set α} (hf : BoundedVariationOn f s) (hg : BoundedVariationOn g s) : BoundedVariationOn (f - g) s

The difference of two bounded-variation functions has bounded variation.

theorem LocallyBoundedVariationOn.sub {α : Type u_1} {E : Type u_2} [LinearOrder α] [SeminormedAddCommGroup E] {f g : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) (hg : LocallyBoundedVariationOn g s) : LocallyBoundedVariationOn (f - g) s

Local bounded variation is stable under subtraction.