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.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.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))

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)

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

Monotone functions and bounded variation

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.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 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