Functions of bounded variation

We study functions of bounded variation. In particular, we show that a bounded variation function is a difference of monotone functions, and differentiable almost everywhere. This implies that Lipschitz functions from the real line into finite-dimensional vector space are also differentiable almost everywhere.

Main definitions and results

• eVariationOn f s is the total variation of the function f on the set s, in ℝ≥0∞.

• BoundedVariationOn f s registers that the variation of f on s is finite.

• LocallyBoundedVariationOn f s registers that f has finite variation on any compact subinterval of s.

• variationOnFromTo f s a b is the signed variation of f on s ∩ Icc a b, converted to ℝ.

• eVariationOn.Icc_add_Icc states that the variation of f on [a, c] is the sum of its variations on [a, b] and [b, c].

• LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn proves that a function with locally bounded variation is the difference of two monotone functions.

• LipschitzWith.locallyBoundedVariationOn shows that a Lipschitz function has locally bounded variation.

We also give several variations around these results.

Implementation

We define the variation as an extended nonnegative real, to allow for infinite variation. This makes it possible to use the complete linear order structure of ℝ≥0∞. The proofs would be much more tedious with an ℝ-valued or ℝ≥0-valued variation, since one would always need to check that the sets one uses are nonempty and bounded above as these are only conditionally complete.

noncomputable def eVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) : ENNReal

The (extended-real-valued) variation of a function f on a set s inside a linear order is the supremum of the sum of edist (f (u (i+1))) (f (u i)) over all finite increasing sequences u in s.

Equations

• eVariationOn f s = ⨆ (p : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }), ∑ i ∈ Finset.range p.1, edist (f (↑p.2 (i + 1))) (f (↑p.2 i))

def BoundedVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) : Prop

A function has bounded variation on a set s if its total variation there is finite.

Equations

• BoundedVariationOn f s = (eVariationOn f s ≠ ⊤)

def LocallyBoundedVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) : Prop

A function has locally bounded variation on a set s if, given any interval [a, b] with endpoints in s, then the function has finite variation on s ∩ [a, b].

Equations

• LocallyBoundedVariationOn f s = ∀ (a b : α), a ∈ s → b ∈ s → BoundedVariationOn f (s ∩ Set.Icc a b)

Basic computations of variation

theorem eVariationOn.nonempty_monotone_mem {α : Type u_1} [LinearOrder α] {s : Set α} (hs : s.Nonempty) : Nonempty { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }

theorem eVariationOn.eq_of_edist_zero_on {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f f' : α → E} {s : Set α} (h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0) : eVariationOn f s = eVariationOn f' s

theorem eVariationOn.eq_of_eqOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f f' : α → E} {s : Set α} (h : Set.EqOn f f' s) : eVariationOn f s = eVariationOn f' s

theorem eVariationOn.sum_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} {n : ℕ} {u : ℕ → α} (hu : Monotone u) (us : ∀ (i : ℕ), u i ∈ s) : ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

theorem eVariationOn.sum_le_of_monotoneOn_Icc {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} {m n : ℕ} {u : ℕ → α} (hu : MonotoneOn u (Set.Icc m n)) (us : ∀ i ∈ Set.Icc m n, u i ∈ s) : ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

theorem eVariationOn.sum_le_of_monotoneOn_Iic {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} {n : ℕ} {u : ℕ → α} (hu : MonotoneOn u (Set.Iic n)) (us : ∀ i ≤ n, u i ∈ s) : ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

theorem eVariationOn.eVariationOn_eq_strictMonoOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) : eVariationOn f s = ⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Set.Iic n) ∧ ∀ i ∈ Set.Iic n, u i ∈ s }), ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i))

The variation can be expressed using strictly monotone functions. This formulation is often less convenient than the one with monotone functions as it involves dependent types, but it is sometimes handy.

theorem eVariationOn.mono {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) {s t : Set α} (hst : t ⊆ s) : eVariationOn f t ≤ eVariationOn f s

theorem BoundedVariationOn.mono {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (h : BoundedVariationOn f s) {t : Set α} (ht : t ⊆ s) : BoundedVariationOn f t

theorem BoundedVariationOn.locallyBoundedVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (h : BoundedVariationOn f s) : LocallyBoundedVariationOn f s

theorem eVariationOn.congr {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f g : α → E} {s : Set α} (h : Set.EqOn f g s) : eVariationOn f s = eVariationOn g s

theorem eVariationOn.edist_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) {s : Set α} {x y : α} (hx : x ∈ s) (hy : y ∈ s) : edist (f x) (f y) ≤ eVariationOn f s

theorem eVariationOn.eq_zero_iff {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) {s : Set α} : eVariationOn f s = 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0

theorem eVariationOn.constant_on {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : (f '' s).Subsingleton) : eVariationOn f s = 0

@[simp]

theorem eVariationOn.subsingleton {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) {s : Set α} (hs : s.Subsingleton) : eVariationOn f s = 0

theorem eVariationOn.lowerSemicontinuous_aux {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {ι : Type u_3} {F : ι → α → E} {p : Filter ι} {f : α → E} {s : Set α} (Ffs : ∀ x ∈ s, Filter.Tendsto (fun (i : ι) => F i x) p (nhds (f x))) {v : ENNReal} (hv : v < eVariationOn f s) : ∀ᶠ (n : ι) in p, v < eVariationOn (F n) s

theorem eVariationOn.lowerSemicontinuous {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (s : Set α) : LowerSemicontinuous fun (f : UniformOnFun α E (singleton '' s)) => eVariationOn f s

The map (eVariationOn · s) is lower semicontinuous for pointwise convergence on s. Pointwise convergence on s is encoded here as uniform convergence on the family consisting of the singletons of elements of s.

theorem eVariationOn.lowerSemicontinuous_uniformOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (s : Set α) : LowerSemicontinuous fun (f : UniformOnFun α E {s}) => eVariationOn f s

The map (eVariationOn · s) is lower semicontinuous for uniform convergence on s.

theorem BoundedVariationOn.dist_le {α : Type u_1} [LinearOrder α] {E : Type u_3} [PseudoMetricSpace E] {f : α → E} {s : Set α} (h : BoundedVariationOn f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : dist (f x) (f y) ≤ (eVariationOn f s).toReal

theorem BoundedVariationOn.sub_le {α : Type u_1} [LinearOrder α] {f : α → ℝ} {s : Set α} (h : BoundedVariationOn f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : f x - f y ≤ (eVariationOn f s).toReal

theorem eVariationOn.add_point {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) {s : Set α} {x : α} (hx : x ∈ s) (u : ℕ → α) (hu : Monotone u) (us : ∀ (i : ℕ), u i ∈ s) (n : ℕ) : ∃ (v : ℕ → α) (m : ℕ), Monotone v ∧ (∀ (i : ℕ), v i ∈ s) ∧ x ∈ v '' Set.Iio m ∧ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))

Consider a monotone function u parameterizing some points of a set s. Given x ∈ s, then one can find another monotone function v parameterizing the same points as u, with x added. In particular, the variation of a function along u is bounded by its variation along v.

theorem eVariationOn.add_le_union {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) {s t : Set α} (h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y) : eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)

The variation of a function on the union of two sets s and t, with s to the left of t, bounds the sum of the variations along s and t.

theorem eVariationOn.union {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) {s t : Set α} {x : α} (hs : IsGreatest s x) (ht : IsLeast t x) : eVariationOn f (s ∪ t) = eVariationOn f s + eVariationOn f t

If a set s is to the left of a set t, and both contain the boundary point x, then the variation of f along s ∪ t is the sum of the variations.

theorem eVariationOn.Icc_add_Icc {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) {s : Set α} {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) (hb : b ∈ s) : eVariationOn f (s ∩ Set.Icc a b) + eVariationOn f (s ∩ Set.Icc b c) = eVariationOn f (s ∩ Set.Icc a c)

theorem eVariationOn.sum {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) {s : Set α} {E✝ : ℕ → α} (hE : Monotone E✝) {n : ℕ} (hn : ∀ (i : ℕ), 0 < i → i < n → E✝ i ∈ s) : ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Set.Icc (E✝ i) (E✝ (i + 1))) = eVariationOn f (s ∩ Set.Icc (E✝ 0) (E✝ n))

theorem eVariationOn.sum' {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) {I : ℕ → α} (hI : Monotone I) {n : ℕ} : ∑ i ∈ Finset.range n, eVariationOn f (Set.Icc (I i) (I (i + 1))) = eVariationOn f (Set.Icc (I 0) (I n))

Composition of bounded variation functions with monotone functions

theorem eVariationOn.comp_le_of_monotoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {β : Type u_3} [LinearOrder β] (f : α → E) {s : Set α} {t : Set β} (φ : β → α) (hφ : MonotoneOn φ t) (φst : Set.MapsTo φ t s) : eVariationOn (f ∘ φ) t ≤ eVariationOn f s

theorem eVariationOn.comp_le_of_antitoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {β : Type u_3} [LinearOrder β] (f : α → E) {s : Set α} {t : Set β} (φ : β → α) (hφ : AntitoneOn φ t) (φst : Set.MapsTo φ t s) : eVariationOn (f ∘ φ) t ≤ eVariationOn f s

theorem eVariationOn.comp_eq_of_monotoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {β : Type u_3} [LinearOrder β] (f : α → E) {t : Set β} (φ : β → α) (hφ : MonotoneOn φ t) : eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t)

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

theorem eVariationOn.comp_eq_of_antitoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {β : Type u_3} [LinearOrder β] (f : α → E) {t : Set β} (φ : β → α) (hφ : AntitoneOn φ t) : eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t)

@[simp]

theorem eVariationOn.comp_ofDual {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) : eVariationOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' s) = eVariationOn f s

theorem BoundedVariationOn.ofDual {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) : BoundedVariationOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' s)

@[simp]

theorem eVariationOn.boundedVariation_ofDual {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} : BoundedVariationOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' s) ↔ BoundedVariationOn f s

Left and right limits of bounded variation functions

theorem eVariationOn.eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} {s : Set α} {a : α} (h : (nhdsWithin a (s ∩ Set.Iio a)).NeBot) (h' : ContinuousWithinAt f (s ∩ Set.Iic a) a) : eVariationOn f (s ∩ Set.Iio a) = eVariationOn f (s ∩ Set.Iic a)

If a function is continuous on the left at a point a, then its variations on Iio a and on Iic a coincide. We give a version relative to a set s.

theorem eVariationOn.eVariationOn_inter_Ioi_eq_inter_Ici_of_continuousWithinAt {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} {s : Set α} {a : α} (h : (nhdsWithin a (s ∩ Set.Ioi a)).NeBot) (h' : ContinuousWithinAt f (s ∩ Set.Ici a) a) : eVariationOn f (s ∩ Set.Ioi a) = eVariationOn f (s ∩ Set.Ici a)

If a function is continuous on the right at a point a, then its variations on Ioi a and on Ici a coincide. We give a version relative to a set s.

theorem eVariationOn.exists_lt_eVariationOn_inter_Icc {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {ε : ENNReal} {s : Set α} (h : ε < eVariationOn f s) : ∃ a ∈ s, ∃ b ∈ s, a < b ∧ ε < eVariationOn f (s ∩ Set.Icc a b)

theorem BoundedVariationOn.tendsto_eVariationOn_Ici_zero_of_filter {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) (L : Filter α) (hL : ∀ y ∈ s, s ∩ Set.Ici y ∈ L) : Filter.Tendsto (fun (y : α) => eVariationOn f (s ∩ Set.Ici y)) L (nhds 0)

If a function has bounded variation, then the variation on closed semi-infinite intervals tends to 0. We give a version with a generic filter, that applies both to left-neighborhoods of points and to atTop.

theorem BoundedVariationOn.exists_tendsto_left_of_filter {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [CompleteSpace E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) (L : Filter α) (hL : ∀ y ∈ s, s ∩ Set.Ici y ∈ L) (hs : s.Nonempty) : ∃ (l : E), Filter.Tendsto f L (nhds l)

A bounded variation function has a limit on its left within a set. Version with a general filter, covering both left neighborhoods of points and atTop.

theorem BoundedVariationOn.tendsto_eVariationOn_Ico_zero {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) (x : α) : Filter.Tendsto (fun (y : α) => eVariationOn f (s ∩ Set.Ico y x)) (nhdsWithin x s) (nhds 0)

If a function has bounded variation, then the variation on small closed-open intervals to the left of any point tends to 0.

theorem BoundedVariationOn.tendsto_eVariationOn_Ioc_zero {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) (x : α) : Filter.Tendsto (fun (y : α) => eVariationOn f (s ∩ Set.Ioc x y)) (nhdsWithin x s) (nhds 0)

If a function has bounded variation, then the variation on small open-closed intervals to the right of any point tends to 0.

theorem BoundedVariationOn.tendsto_eVariationOn_Icc_zero_left {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) {x : α} (h : ContinuousWithinAt f (s ∩ Set.Iic x) x) : Filter.Tendsto (fun (y : α) => eVariationOn f (s ∩ Set.Icc y x)) (nhdsWithin x s) (nhds 0)

If a function has bounded variation and is left-continuous at a point, then the variation on small closed intervals to the left of this point tends to 0.

theorem BoundedVariationOn.tendsto_eVariationOn_Icc_zero_right {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) (x : α) (h : ContinuousWithinAt f (s ∩ Set.Ici x) x) : Filter.Tendsto (fun (y : α) => eVariationOn f (s ∩ Set.Icc x y)) (nhdsWithin x s) (nhds 0)

If a function has bounded variation and is right-continuous at a point, then the variation on small closed intervals to the right of this point tends to 0.

theorem BoundedVariationOn.exists_tendsto_left {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [CompleteSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) (x : α) : ∃ (l : E), Filter.Tendsto f (nhdsWithin x (s ∩ Set.Iio x)) (nhds l)

A bounded variation function has a limit on its left within a set.

theorem BoundedVariationOn.exists_tendsto_right {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [CompleteSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) (x : α) : ∃ (l : E), Filter.Tendsto f (nhdsWithin x (s ∩ Set.Ioi x)) (nhds l)

A bounded variation function has a limit on its right within a set.

theorem BoundedVariationOn.tendsto_leftLim {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [CompleteSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} (hf : BoundedVariationOn f Set.univ) (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (Function.leftLim f x))

A bounded variation function tends to its left-limit on its left.

theorem BoundedVariationOn.tendsto_rightLim {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [CompleteSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} (hf : BoundedVariationOn f Set.univ) (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (Function.rightLim f x))

A bounded variation function tends to its right-limit on its right.

theorem eVariationOn.eVariationOn_leftLim_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} : eVariationOn (Function.leftLim f) Set.univ ≤ eVariationOn f Set.univ

theorem eVariationOn.eVariationOn_rightLim_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} : eVariationOn (Function.rightLim f) Set.univ ≤ eVariationOn f Set.univ

theorem BoundedVariationOn.leftLim {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} (hf : BoundedVariationOn f Set.univ) : BoundedVariationOn (Function.leftLim f) Set.univ

theorem BoundedVariationOn.rightLim {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} (hf : BoundedVariationOn f Set.univ) : BoundedVariationOn (Function.rightLim f) Set.univ

theorem BoundedVariationOn.continuousWithinAt_leftLim {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [TopologicalSpace α] [OrderTopology α] [CompleteSpace E] [T3Space E] {f : α → E} (hf : BoundedVariationOn f Set.univ) {x : α} : ContinuousWithinAt (Function.leftLim f) (Set.Iic x) x

theorem BoundedVariationOn.continuousWithinAt_rightLim {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [TopologicalSpace α] [OrderTopology α] [CompleteSpace E] [T3Space E] {f : α → E} (hf : BoundedVariationOn f Set.univ) {x : α} : ContinuousWithinAt (Function.rightLim f) (Set.Ici x) x

Limits of bounded variation functions as ± ∞

theorem BoundedVariationOn.tendsto_eVariationOn_Ici_zero {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) : Filter.Tendsto (fun (y : α) => eVariationOn f (s ∩ Set.Ici y)) (Filter.principal s ⊓ Filter.atTop) (nhds 0)

If a function has bounded variation, then the variation on closed semi-infinite intervals tends to 0 at +∞.

theorem BoundedVariationOn.tendsto_eVariationOn_Iic_zero {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) : Filter.Tendsto (fun (y : α) => eVariationOn f (s ∩ Set.Iic y)) (Filter.principal s ⊓ Filter.atBot) (nhds 0)

If a function has bounded variation, then the variation on semi-infinite closed intervals tends to 0 at -∞.

theorem BoundedVariationOn.exists_tendsto_atTop {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [CompleteSpace E] [hE : Nonempty E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) : ∃ (l : E), Filter.Tendsto f (Filter.principal s ⊓ Filter.atTop) (nhds l)

A bounded variation function has a limit at +∞.

theorem BoundedVariationOn.exists_tendsto_atBot {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [CompleteSpace E] [hE : Nonempty E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) : ∃ (l : E), Filter.Tendsto f (Filter.principal s ⊓ Filter.atBot) (nhds l)

A bounded variation function has a limit at -∞.

theorem BoundedVariationOn.tendsto_atTop_limUnder {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [CompleteSpace E] [hE : Nonempty E] {f : α → E} (hf : BoundedVariationOn f Set.univ) : Filter.Tendsto f Filter.atTop (nhds (limUnder Filter.atTop f))

theorem BoundedVariationOn.tendsto_atBot_limUnder {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] [CompleteSpace E] [hE : Nonempty E] {f : α → E} (hf : BoundedVariationOn f Set.univ) : Filter.Tendsto f Filter.atBot (nhds (limUnder Filter.atBot f))

Variation of monotone functions

theorem MonotoneOn.eVariationOn_le {α : Type u_1} [LinearOrder α] {f : α → ℝ} {s : Set α} (hf : MonotoneOn f s) {a b : α} (as : a ∈ s) (bs : b ∈ s) : eVariationOn f (s ∩ Set.Icc a b) ≤ ENNReal.ofReal (f b - f a)

theorem MonotoneOn.locallyBoundedVariationOn {α : Type u_1} [LinearOrder α] {f : α → ℝ} {s : Set α} (hf : MonotoneOn f s) : LocallyBoundedVariationOn f s

noncomputable def variationOnFromTo {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) (a b : α) : ℝ

The signed variation of f on the interval Icc a b intersected with the set s, squashed to a real (therefore only really meaningful if the variation is finite)

Equations

• variationOnFromTo f s a b = if a ≤ b then (eVariationOn f (s ∩ Set.Icc a b)).toReal else -(eVariationOn f (s ∩ Set.Icc b a)).toReal

theorem variationOnFromTo.self {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) (a : α) : variationOnFromTo f s a a = 0

theorem variationOnFromTo.nonneg_of_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) {a b : α} (h : a ≤ b) : 0 ≤ variationOnFromTo f s a b

theorem variationOnFromTo.eq_neg_swap {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) (a b : α) : variationOnFromTo f s a b = -variationOnFromTo f s b a

theorem variationOnFromTo.nonpos_of_ge {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) {a b : α} (h : b ≤ a) : variationOnFromTo f s a b ≤ 0

theorem variationOnFromTo.abs_le_eVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) {a b : α} : |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal

theorem variationOnFromTo.eq_of_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) {a b : α} (h : a ≤ b) : variationOnFromTo f s a b = (eVariationOn f (s ∩ Set.Icc a b)).toReal

theorem variationOnFromTo.eq_of_ge {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) (s : Set α) {a b : α} (h : b ≤ a) : variationOnFromTo f s a b = -(eVariationOn f (s ∩ Set.Icc b a)).toReal

theorem variationOnFromTo.add {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b c : α} (ha : a ∈ s) (hb : b ∈ s) (hc : c ∈ s) : variationOnFromTo f s a b + variationOnFromTo f s b c = variationOnFromTo f s a c

theorem variationOnFromTo.edist_zero_of_eq_zero {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : variationOnFromTo f s a b = 0) : edist (f a) (f b) = 0

theorem variationOnFromTo.eq_left_iff {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b c : α} (ha : a ∈ s) (hb : b ∈ s) (hc : c ∈ s) : variationOnFromTo f s a b = variationOnFromTo f s a c ↔ variationOnFromTo f s b c = 0

theorem variationOnFromTo.eq_zero_iff_of_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (ab : a ≤ b) : variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Set.Icc a b → ∀ ⦃y : α⦄, y ∈ s ∩ Set.Icc a b → edist (f x) (f y) = 0

theorem variationOnFromTo.eq_zero_iff_of_ge {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (ba : b ≤ a) : variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Set.Icc b a → ∀ ⦃y : α⦄, y ∈ s ∩ Set.Icc b a → edist (f x) (f y) = 0

theorem variationOnFromTo.eq_zero_iff {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Set.uIcc a b → ∀ ⦃y : α⦄, y ∈ s ∩ Set.uIcc a b → edist (f x) (f y) = 0

theorem variationOnFromTo.monotoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} (as : a ∈ s) : MonotoneOn (variationOnFromTo f s a) s

theorem variationOnFromTo.antitoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {b : α} (bs : b ∈ s) : AntitoneOn (fun (a : α) => variationOnFromTo f s a b) s

theorem variationOnFromTo.sub_self_monotoneOn {α : Type u_1} [LinearOrder α] {f : α → ℝ} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} (as : a ∈ s) : MonotoneOn (variationOnFromTo f s a - f) s

theorem variationOnFromTo.comp_eq_of_monotoneOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {β : Type u_3} [LinearOrder β] (f : α → E) {t : Set β} (φ : β → α) (hφ : MonotoneOn φ t) {x y : β} (hx : x ∈ t) (hy : y ∈ t) : variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_Ici {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} [TopologicalSpace α] [OrderTopology α] (hf : BoundedVariationOn f Set.univ) {a x : α} (hx : ContinuousWithinAt f (Set.Ici x) x) : ContinuousWithinAt (variationOnFromTo f Set.univ a) (Set.Ici x) x

theorem BoundedVariationOn.continuousWithinAt_variationOnFromTo_rightLim_Ici {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} [TopologicalSpace α] [OrderTopology α] [T3Space E] [CompleteSpace E] (hf : BoundedVariationOn f Set.univ) {a x : α} : ContinuousWithinAt (variationOnFromTo (Function.rightLim f) Set.univ a) (Set.Ici x) x

theorem LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn {α : Type u_1} [LinearOrder α] {f : α → ℝ} {s : Set α} (h : LocallyBoundedVariationOn f s) : ∃ (p : α → ℝ) (q : α → ℝ), MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q

If a real-valued function has bounded variation on a set, then it is a difference of monotone functions there.

Lipschitz functions and bounded variation

theorem LipschitzOnWith.comp_eVariationOn_le {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {F : Type u_3} [PseudoEMetricSpace F] {f : E → F} {C : NNReal} {t : Set E} (h : LipschitzOnWith C f t) {g : α → E} {s : Set α} (hg : Set.MapsTo g s t) : eVariationOn (f ∘ g) s ≤ ↑C * eVariationOn g s

theorem LipschitzOnWith.comp_boundedVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {F : Type u_3} [PseudoEMetricSpace F] {f : E → F} {C : NNReal} {t : Set E} (hf : LipschitzOnWith C f t) {g : α → E} {s : Set α} (hg : Set.MapsTo g s t) (h : BoundedVariationOn g s) : BoundedVariationOn (f ∘ g) s

theorem LipschitzOnWith.comp_locallyBoundedVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {F : Type u_3} [PseudoEMetricSpace F] {f : E → F} {C : NNReal} {t : Set E} (hf : LipschitzOnWith C f t) {g : α → E} {s : Set α} (hg : Set.MapsTo g s t) (h : LocallyBoundedVariationOn g s) : LocallyBoundedVariationOn (f ∘ g) s

theorem LipschitzWith.comp_boundedVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {F : Type u_3} [PseudoEMetricSpace F] {f : E → F} {C : NNReal} (hf : LipschitzWith C f) {g : α → E} {s : Set α} (h : BoundedVariationOn g s) : BoundedVariationOn (f ∘ g) s

theorem LipschitzWith.comp_locallyBoundedVariationOn {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {F : Type u_3} [PseudoEMetricSpace F] {f : E → F} {C : NNReal} (hf : LipschitzWith C f) {g : α → E} {s : Set α} (h : LocallyBoundedVariationOn g s) : LocallyBoundedVariationOn (f ∘ g) s

theorem LipschitzOnWith.locallyBoundedVariationOn {E : Type u_2} [PseudoEMetricSpace E] {f : ℝ → E} {C : NNReal} {s : Set ℝ} (hf : LipschitzOnWith C f s) : LocallyBoundedVariationOn f s

theorem LipschitzWith.locallyBoundedVariationOn {E : Type u_2} [PseudoEMetricSpace E] {f : ℝ → E} {C : NNReal} (hf : LipschitzWith C f) (s : Set ℝ) : LocallyBoundedVariationOn f s