# Documentation

Mathlib.Analysis.BoundedVariation

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

• LocallyBoundedVariationOn.ae_differentiableWithinAt shows that a bounded variation function into a finite dimensional real vector space is differentiable almost everywhere.

• LipschitzOnWith.ae_differentiableWithinAt is the same result for Lipschitz functions.

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} [] {E : Type u_2} (f : αE) (s : Set α) :

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.

Instances For
def BoundedVariationOn {α : Type u_1} [] {E : Type u_2} (f : αE) (s : Set α) :

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

Instances For
def LocallyBoundedVariationOn {α : Type u_1} [] {E : Type u_2} (f : αE) (s : Set α) :

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

Instances For

## Basic computations of variation #

theorem eVariationOn.nonempty_monotone_mem {α : Type u_1} [] {s : Set α} (hs : ) :
Nonempty { u // ∀ (i : ), u i s }
theorem eVariationOn.eq_of_edist_zero_on {α : Type u_1} [] {E : Type u_2} {f : αE} {f' : αE} {s : Set α} (h : ∀ ⦃x : α⦄, x sedist (f x) (f' x) = 0) :
theorem eVariationOn.eq_of_eqOn {α : Type u_1} [] {E : Type u_2} {f : αE} {f' : αE} {s : Set α} (h : Set.EqOn f f' s) :
theorem eVariationOn.sum_le {α : Type u_1} [] {E : Type u_2} (f : αE) {s : Set α} (n : ) {u : α} (hu : ) (us : ∀ (i : ), u i s) :
(Finset.sum () fun i => edist (f (u (i + 1))) (f (u i)))
theorem eVariationOn.sum_le_of_monotoneOn_Icc {α : Type u_1} [] {E : Type u_2} (f : αE) {s : Set α} {m : } {n : } {u : α} (hu : MonotoneOn u (Set.Icc m n)) (us : ∀ (i : ), i Set.Icc m nu i s) :
(Finset.sum () fun i => edist (f (u (i + 1))) (f (u i)))
theorem eVariationOn.sum_le_of_monotoneOn_Iic {α : Type u_1} [] {E : Type u_2} (f : αE) {s : Set α} {n : } {u : α} (hu : MonotoneOn u ()) (us : ∀ (i : ), i nu i s) :
(Finset.sum () fun i => edist (f (u (i + 1))) (f (u i)))
theorem eVariationOn.mono {α : Type u_1} [] {E : Type u_2} (f : αE) {s : Set α} {t : Set α} (hst : t s) :
theorem BoundedVariationOn.mono {α : Type u_1} [] {E : Type u_2} {f : αE} {s : Set α} (h : ) {t : Set α} (ht : t s) :
theorem BoundedVariationOn.locallyBoundedVariationOn {α : Type u_1} [] {E : Type u_2} {f : αE} {s : Set α} (h : ) :
theorem eVariationOn.edist_le {α : Type u_1} [] {E : Type u_2} (f : αE) {s : Set α} {x : α} {y : α} (hx : x s) (hy : y s) :
edist (f x) (f y)
theorem eVariationOn.eq_zero_iff {α : Type u_1} [] {E : Type u_2} (f : αE) {s : Set α} :
= 0 ∀ (x : α), x s∀ (y : α), y sedist (f x) (f y) = 0
theorem eVariationOn.constant_on {α : Type u_1} [] {E : Type u_2} {f : αE} {s : Set α} (hf : Set.Subsingleton (f '' s)) :
= 0
@[simp]
theorem eVariationOn.subsingleton {α : Type u_1} [] {E : Type u_2} (f : αE) {s : Set α} (hs : ) :
= 0
theorem eVariationOn.lowerSemicontinuous_aux {α : Type u_1} [] {E : Type u_2} {ι : Type u_3} {F : ιαE} {p : } {f : αE} {s : Set α} (Ffs : ∀ (x : α), x sFilter.Tendsto (fun i => F i x) p (nhds (f x))) {v : ENNReal} (hv : v < ) :
∀ᶠ (n : ι) in p, v < eVariationOn (F n) s
theorem eVariationOn.lowerSemicontinuous {α : Type u_1} [] {E : Type u_2} (s : Set α) :

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} [] {E : Type u_2} (s : Set α) :

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

theorem BoundedVariationOn.dist_le {α : Type u_1} [] {E : Type u_3} {f : αE} {s : Set α} (h : ) {x : α} {y : α} (hx : x s) (hy : y s) :
dist (f x) (f y)
theorem BoundedVariationOn.sub_le {α : Type u_1} [] {f : α} {s : Set α} (h : ) {x : α} {y : α} (hx : x s) (hy : y s) :
f x - f y
theorem eVariationOn.add_point {α : Type u_1} [] {E : Type u_2} (f : αE) {s : Set α} {x : α} (hx : x s) (u : α) (hu : ) (us : ∀ (i : ), u i s) (n : ) :
v m, (∀ (i : ), v i s) x v '' (Finset.sum () fun i => edist (f (u (i + 1))) (f (u i))) Finset.sum () fun j => 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} [] {E : Type u_2} (f : αE) {s : Set α} {t : Set α} (h : ∀ (x : α), x s∀ (y : α), y tx y) :

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} [] {E : Type u_2} (f : αE) {s : Set α} {t : Set α} {x : α} (hs : ) (ht : IsLeast t x) :
eVariationOn f (s 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} [] {E : Type u_2} (f : αE) {s : Set α} {a : α} {b : α} {c : α} (hab : a b) (hbc : b c) (hb : b s) :
theorem eVariationOn.comp_le_of_monotoneOn {α : Type u_1} [] {E : Type u_2} {β : Type u_3} [] (f : αE) {s : Set α} {t : Set β} (φ : βα) (hφ : ) (φst : Set.MapsTo φ t s) :
eVariationOn (f φ) t
theorem eVariationOn.comp_le_of_antitoneOn {α : Type u_1} [] {E : Type u_2} {β : Type u_3} [] (f : αE) {s : Set α} {t : Set β} (φ : βα) (hφ : ) (φst : Set.MapsTo φ t s) :
eVariationOn (f φ) t
theorem eVariationOn.comp_eq_of_monotoneOn {α : Type u_1} [] {E : Type u_2} {β : Type u_3} [] (f : αE) {t : Set β} (φ : βα) (hφ : ) :
eVariationOn (f φ) t = eVariationOn f (φ '' t)
theorem eVariationOn.comp_inter_Icc_eq_of_monotoneOn {α : Type u_1} [] {E : Type u_2} {β : Type u_3} [] (f : αE) {t : Set β} (φ : βα) (hφ : ) {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} [] {E : Type u_2} {β : Type u_3} [] (f : αE) {t : Set β} (φ : βα) (hφ : ) :
eVariationOn (f φ) t = eVariationOn f (φ '' t)
theorem eVariationOn.comp_ofDual {α : Type u_1} [] {E : Type u_2} (f : αE) (s : Set α) :
eVariationOn (f OrderDual.ofDual) (OrderDual.ofDual ⁻¹' s) =

## Monotone functions and bounded variation #

theorem MonotoneOn.eVariationOn_le {α : Type u_1} [] {f : α} {s : Set α} (hf : ) {a : α} {b : α} (as : a s) (bs : b s) :
theorem MonotoneOn.locallyBoundedVariationOn {α : Type u_1} [] {f : α} {s : Set α} (hf : ) :
noncomputable def variationOnFromTo {α : Type u_1} [] {E : Type u_2} (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)

Instances For
theorem variationOnFromTo.self {α : Type u_1} [] {E : Type u_2} (f : αE) (s : Set α) (a : α) :
= 0
theorem variationOnFromTo.nonneg_of_le {α : Type u_1} [] {E : Type u_2} (f : αE) (s : Set α) {a : α} {b : α} (h : a b) :
0
theorem variationOnFromTo.eq_neg_swap {α : Type u_1} [] {E : Type u_2} (f : αE) (s : Set α) (a : α) (b : α) :
= -
theorem variationOnFromTo.nonpos_of_ge {α : Type u_1} [] {E : Type u_2} (f : αE) (s : Set α) {a : α} {b : α} (h : b a) :
0
theorem variationOnFromTo.eq_of_le {α : Type u_1} [] {E : Type u_2} (f : αE) (s : Set α) {a : α} {b : α} (h : a b) :
theorem variationOnFromTo.eq_of_ge {α : Type u_1} [] {E : Type u_2} (f : αE) (s : Set α) {a : α} {b : α} (h : b a) :
theorem variationOnFromTo.add {α : Type u_1} [] {E : Type u_2} {f : αE} {s : Set α} (hf : ) {a : α} {b : α} {c : α} (ha : a s) (hb : b s) (hc : c s) :
+ =
theorem variationOnFromTo.edist_zero_of_eq_zero {α : Type u_1} [] {E : Type u_2} {f : αE} {s : Set α} (hf : ) {a : α} {b : α} (ha : a s) (hb : b s) (h : = 0) :
edist (f a) (f b) = 0
theorem variationOnFromTo.eq_left_iff {α : Type u_1} [] {E : Type u_2} {f : αE} {s : Set α} (hf : ) {a : α} {b : α} {c : α} (ha : a s) (hb : b s) (hc : c s) :
= = 0
theorem variationOnFromTo.eq_zero_iff_of_le {α : Type u_1} [] {E : Type u_2} {f : αE} {s : Set α} (hf : ) {a : α} {b : α} (ha : a s) (hb : b s) (ab : a b) :
= 0 ∀ ⦃x : α⦄, x s Set.Icc a b∀ ⦃y : α⦄, y s Set.Icc a bedist (f x) (f y) = 0
theorem variationOnFromTo.eq_zero_iff_of_ge {α : Type u_1} [] {E : Type u_2} {f : αE} {s : Set α} (hf : ) {a : α} {b : α} (ha : a s) (hb : b s) (ba : b a) :
= 0 ∀ ⦃x : α⦄, x s Set.Icc b a∀ ⦃y : α⦄, y s Set.Icc b aedist (f x) (f y) = 0
theorem variationOnFromTo.eq_zero_iff {α : Type u_1} [] {E : Type u_2} {f : αE} {s : Set α} (hf : ) {a : α} {b : α} (ha : a s) (hb : b s) :
= 0 ∀ ⦃x : α⦄, x s Set.uIcc a b∀ ⦃y : α⦄, y s Set.uIcc a bedist (f x) (f y) = 0
theorem variationOnFromTo.monotoneOn {α : Type u_1} [] {E : Type u_2} {f : αE} {s : Set α} (hf : ) {a : α} (as : a s) :
theorem variationOnFromTo.antitoneOn {α : Type u_1} [] {E : Type u_2} {f : αE} {s : Set α} (hf : ) {b : α} (bs : b s) :
AntitoneOn (fun a => ) s
theorem variationOnFromTo.sub_self_monotoneOn {α : Type u_1} [] {f : α} {s : Set α} (hf : ) {a : α} (as : a s) :
MonotoneOn ( - f) s
theorem variationOnFromTo.comp_eq_of_monotoneOn {α : Type u_1} [] {E : Type u_2} {β : Type u_3} [] (f : αE) {t : Set β} (φ : βα) (hφ : ) {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} [] {f : α} {s : Set α} (h : ) :
p q, 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} [] {E : Type u_2} {F : Type u_3} {f : EF} {C : NNReal} {t : Set E} (h : ) {g : αE} {s : Set α} (hg : Set.MapsTo g s t) :
eVariationOn (f g) s C *
theorem LipschitzOnWith.comp_boundedVariationOn {α : Type u_1} [] {E : Type u_2} {F : Type u_3} {f : EF} {C : NNReal} {t : Set E} (hf : ) {g : αE} {s : Set α} (hg : Set.MapsTo g s t) (h : ) :
theorem LipschitzOnWith.comp_locallyBoundedVariationOn {α : Type u_1} [] {E : Type u_2} {F : Type u_3} {f : EF} {C : NNReal} {t : Set E} (hf : ) {g : αE} {s : Set α} (hg : Set.MapsTo g s t) (h : ) :
theorem LipschitzWith.comp_boundedVariationOn {α : Type u_1} [] {E : Type u_2} {F : Type u_3} {f : EF} {C : NNReal} (hf : ) {g : αE} {s : Set α} (h : ) :
theorem LipschitzWith.comp_locallyBoundedVariationOn {α : Type u_1} [] {E : Type u_2} {F : Type u_3} {f : EF} {C : NNReal} (hf : ) {g : αE} {s : Set α} (h : ) :
theorem LipschitzOnWith.locallyBoundedVariationOn {E : Type u_2} {f : E} {C : NNReal} {s : } (hf : ) :
theorem LipschitzWith.locallyBoundedVariationOn {E : Type u_2} {f : E} {C : NNReal} (hf : ) (s : ) :

## Almost everywhere differentiability of functions with locally bounded variation #

theorem LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_real {f : } {s : } (h : ) :
∀ᵐ (x : ), x s

A bounded variation function into ℝ is differentiable almost everywhere. Superseded by ae_differentiableWithinAt_of_mem.

theorem LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_pi {ι : Type u_4} [] {f : ι} {s : } (h : ) :
∀ᵐ (x : ), x s

A bounded variation function into a finite dimensional product vector space is differentiable almost everywhere. Superseded by ae_differentiableWithinAt_of_mem.

theorem LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem {V : Type u_3} [] [] {f : V} {s : } (h : ) :
∀ᵐ (x : ), x s

A real function into a finite dimensional real vector space with bounded variation on a set is differentiable almost everywhere in this set.

theorem LocallyBoundedVariationOn.ae_differentiableWithinAt {V : Type u_3} [] [] {f : V} {s : } (h : ) (hs : ) :
∀ᵐ (x : ) ∂MeasureTheory.Measure.restrict MeasureTheory.volume s,

A real function into a finite dimensional real vector space with bounded variation on a set is differentiable almost everywhere in this set.

theorem LocallyBoundedVariationOn.ae_differentiableAt {V : Type u_3} [] [] {f : V} (h : LocallyBoundedVariationOn f Set.univ) :
∀ᵐ (x : ),

A real function into a finite dimensional real vector space with bounded variation is differentiable almost everywhere.

theorem LipschitzOnWith.ae_differentiableWithinAt_of_mem {V : Type u_3} [] [] {C : NNReal} {f : V} {s : } (h : ) :
∀ᵐ (x : ), x s

A real function into a finite dimensional real vector space which is Lipschitz on a set is differentiable almost everywhere in this set .

theorem LipschitzOnWith.ae_differentiableWithinAt {V : Type u_3} [] [] {C : NNReal} {f : V} {s : } (h : ) (hs : ) :
∀ᵐ (x : ) ∂MeasureTheory.Measure.restrict MeasureTheory.volume s,

A real function into a finite dimensional real vector space which is Lipschitz on a set is differentiable almost everywhere in this set.

theorem LipschitzWith.ae_differentiableAt {V : Type u_3} [] [] {C : NNReal} {f : V} (h : ) :
∀ᵐ (x : ),

A real Lipschitz function into a finite dimensional real vector space is differentiable almost everywhere.