# mathlib3documentation

analysis.bounded_variation

# Functions of bounded variation #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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

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

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

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

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

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

• lipschitz_with.has_locally_bounded_variation_on shows that a Lipschitz function has locally bounded variation.

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

• lipschitz_on_with.ae_differentiable_within_at 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 evariation_on {α : Type u_1} [linear_order α] {E : Type u_3} (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.

Equations
def has_bounded_variation_on {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) (s : set α) :
Prop

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

Equations
def has_locally_bounded_variation_on {α : Type u_1} [linear_order α] {E : Type u_3} (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

## Basic computations of variation #

theorem evariation_on.nonempty_monotone_mem {α : Type u_1} [linear_order α] {s : set α} (hs : s.nonempty) :
nonempty {u // (i : ), u i s}
theorem evariation_on.eq_of_edist_zero_on {α : Type u_1} [linear_order α] {E : Type u_3} {f f' : α E} {s : set α} (h : ⦃x : α⦄, x s has_edist.edist (f x) (f' x) = 0) :
= s
theorem evariation_on.eq_of_eq_on {α : Type u_1} [linear_order α] {E : Type u_3} {f f' : α E} {s : set α} (h : f' s) :
= s
theorem evariation_on.sum_le {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) {s : set α} (n : ) {u : α} (hu : monotone u) (us : (i : ), u i s) :
(finset.range n).sum (λ (i : ), has_edist.edist (f (u (i + 1))) (f (u i)))
theorem evariation_on.sum_le_of_monotone_on_Iic {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) {s : set α} {n : } {u : α} (hu : (set.Iic n)) (us : (i : ), i n u i s) :
(finset.range n).sum (λ (i : ), has_edist.edist (f (u (i + 1))) (f (u i)))
theorem evariation_on.sum_le_of_monotone_on_Icc {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) {s : set α} {m n : } {u : α} (hu : (set.Icc m n)) (us : (i : ), i n u i s) :
n).sum (λ (i : ), has_edist.edist (f (u (i + 1))) (f (u i)))
theorem evariation_on.mono {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) {s t : set α} (hst : t s) :
theorem has_bounded_variation_on.mono {α : Type u_1} [linear_order α] {E : Type u_3} {f : α E} {s : set α} (h : s) {t : set α} (ht : t s) :
theorem has_bounded_variation_on.has_locally_bounded_variation_on {α : Type u_1} [linear_order α] {E : Type u_3} {f : α E} {s : set α} (h : s) :
theorem evariation_on.edist_le {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) {s : set α} {x y : α} (hx : x s) (hy : y s) :
has_edist.edist (f x) (f y)
theorem evariation_on.eq_zero_iff {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) {s : set α} :
= 0 (x : α), x s (y : α), y s has_edist.edist (f x) (f y) = 0
theorem evariation_on.constant_on {α : Type u_1} [linear_order α] {E : Type u_3} {f : α E} {s : set α} (hf : (f '' s).subsingleton) :
= 0
@[protected, simp]
theorem evariation_on.subsingleton {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) {s : set α} (hs : s.subsingleton) :
= 0
theorem evariation_on.lower_continuous_aux {α : Type u_1} [linear_order α] {E : Type u_3} {ι : Type u_2} {F : ι α E} {p : filter ι} {f : α E} {s : set α} (Ffs : (x : α), x s filter.tendsto (λ (i : ι), F i x) p (nhds (f x))) {v : ennreal} (hv : v < ) :
∀ᶠ (n : ι) in p, v < evariation_on (F n) s
@[protected]
theorem evariation_on.lower_semicontinuous {α : Type u_1} [linear_order α] {E : Type u_3} (s : set α) :
lower_semicontinuous (λ (f : , s)

The map λ f, evariation_on f 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 evariation_on.lower_semicontinuous_uniform_on {α : Type u_1} [linear_order α] {E : Type u_3} (s : set α) :
lower_semicontinuous (λ (f : {s}), s)

The map λ f, evariation_on f s is lower semicontinuous for uniform convergence on s.

theorem has_bounded_variation_on.dist_le {α : Type u_1} [linear_order α] {E : Type u_2} {f : α E} {s : set α} (h : s) {x y : α} (hx : x s) (hy : y s) :
has_dist.dist (f x) (f y) s).to_real
theorem has_bounded_variation_on.sub_le {α : Type u_1} [linear_order α] {f : α } {s : set α} (h : s) {x y : α} (hx : x s) (hy : y s) :
f x - f y s).to_real
theorem evariation_on.add_point {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) {s : set α} {x : α} (hx : x s) (u : α) (hu : monotone u) (us : (i : ), u i s) (n : ) :
(v : α) (m : ), ( (i : ), v i s) x v '' (finset.range n).sum (λ (i : ), has_edist.edist (f (u (i + 1))) (f (u i))) (finset.range m).sum (λ (j : ), has_edist.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 evariation_on.add_le_union {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) {s t : set α} (h : (x : α), x s (y : α), y t x y) :
+ (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 evariation_on.union {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) {s t : set α} {x : α} (hs : x) (ht : x) :
(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 evariation_on.Icc_add_Icc {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) {s : set α} {a b c : α} (hab : a b) (hbc : b c) (hb : b s) :
(s b) + (s c) = (s c)
theorem evariation_on.comp_le_of_monotone_on {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {E : Type u_3} (f : α E) {s : set α} {t : set β} (φ : β α) (hφ : t) (φst : t s) :
theorem evariation_on.comp_le_of_antitone_on {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {E : Type u_3} (f : α E) {s : set α} {t : set β} (φ : β α) (hφ : t) (φst : t s) :
theorem evariation_on.comp_eq_of_monotone_on {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {E : Type u_3} (f : α E) {t : set β} (φ : β α) (hφ : t) :
evariation_on (f φ) t = '' t)
theorem set.subsingleton_Icc_of_ge {α : Type u_1} {a b : α} (h : b a) :
theorem evariation_on.comp_inter_Icc_eq_of_monotone_on {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {E : Type u_3} (f : α E) {t : set β} (φ : β α) (hφ : t) {x y : β} (hx : x t) (hy : y t) :
evariation_on (f φ) (t y) = '' t set.Icc (φ x) (φ y))
theorem evariation_on.comp_eq_of_antitone_on {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {E : Type u_3} (f : α E) {t : set β} (φ : β α) (hφ : t) :
evariation_on (f φ) t = '' t)
theorem evariation_on.comp_of_dual {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) (s : set α) :

## Monotone functions and bounded variation #

theorem monotone_on.evariation_on_le {α : Type u_1} [linear_order α] {f : α } {s : set α} (hf : s) {a b : α} (as : a s) (bs : b s) :
(s b) ennreal.of_real (f b - f a)
theorem monotone_on.has_locally_bounded_variation_on {α : Type u_1} [linear_order α] {f : α } {s : set α} (hf : s) :
noncomputable def variation_on_from_to {α : Type u_1} [linear_order α] {E : Type u_3} (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
@[protected]
theorem variation_on_from_to.self {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) (s : set α) (a : α) :
a a = 0
@[protected]
theorem variation_on_from_to.nonneg_of_le {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) (s : set α) {a b : α} (h : a b) :
0 a b
@[protected]
theorem variation_on_from_to.eq_neg_swap {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) (s : set α) (a b : α) :
a b = - b a
@[protected]
theorem variation_on_from_to.nonpos_of_ge {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) (s : set α) {a b : α} (h : b a) :
a b 0
@[protected]
theorem variation_on_from_to.eq_of_le {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) (s : set α) {a b : α} (h : a b) :
a b = (s b)).to_real
@[protected]
theorem variation_on_from_to.eq_of_ge {α : Type u_1} [linear_order α] {E : Type u_3} (f : α E) (s : set α) {a b : α} (h : b a) :
a b = - (s a)).to_real
@[protected]
theorem variation_on_from_to.add {α : Type u_1} [linear_order α] {E : Type u_3} {f : α E} {s : set α} (hf : s) {a b c : α} (ha : a s) (hb : b s) (hc : c s) :
a b + b c = a c
@[protected]
theorem variation_on_from_to.edist_zero_of_eq_zero {α : Type u_1} [linear_order α] {E : Type u_3} {f : α E} {s : set α} (hf : s) {a b : α} (ha : a s) (hb : b s) (h : a b = 0) :
has_edist.edist (f a) (f b) = 0
@[protected]
theorem variation_on_from_to.eq_left_iff {α : Type u_1} [linear_order α] {E : Type u_3} {f : α E} {s : set α} (hf : s) {a b c : α} (ha : a s) (hb : b s) (hc : c s) :
a b = a c b c = 0
@[protected]
theorem variation_on_from_to.eq_zero_iff_of_le {α : Type u_1} [linear_order α] {E : Type u_3} {f : α E} {s : set α} (hf : s) {a b : α} (ha : a s) (hb : b s) (ab : a b) :
a b = 0 ⦃x : α⦄, x s b ⦃y : α⦄, y s b has_edist.edist (f x) (f y) = 0
@[protected]
theorem variation_on_from_to.eq_zero_iff_of_ge {α : Type u_1} [linear_order α] {E : Type u_3} {f : α E} {s : set α} (hf : s) {a b : α} (ha : a s) (hb : b s) (ba : b a) :
a b = 0 ⦃x : α⦄, x s a ⦃y : α⦄, y s a has_edist.edist (f x) (f y) = 0
@[protected]
theorem variation_on_from_to.eq_zero_iff {α : Type u_1} [linear_order α] {E : Type u_3} {f : α E} {s : set α} (hf : s) {a b : α} (ha : a s) (hb : b s) :
a b = 0 ⦃x : α⦄, x s b ⦃y : α⦄, y s b has_edist.edist (f x) (f y) = 0
@[protected]
theorem variation_on_from_to.monotone_on {α : Type u_1} [linear_order α] {E : Type u_3} {f : α E} {s : set α} (hf : s) {a : α} (as : a s) :
@[protected]
theorem variation_on_from_to.antitone_on {α : Type u_1} [linear_order α] {E : Type u_3} {f : α E} {s : set α} (hf : s) {b : α} (bs : b s) :
antitone_on (λ (a : α), a b) s
@[protected]
theorem variation_on_from_to.sub_self_monotone_on {α : Type u_1} [linear_order α] {f : α } {s : set α} (hf : s) {a : α} (as : a s) :
monotone_on a - f) s
@[protected]
theorem variation_on_from_to.comp_eq_of_monotone_on {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {E : Type u_3} (f : α E) {t : set β} (φ : β α) (hφ : t) {x y : β} (hx : x t) (hy : y t) :
variation_on_from_to (f φ) t x y = '' t) (φ x) (φ y)
theorem has_locally_bounded_variation_on.exists_monotone_on_sub_monotone_on {α : Type u_1} [linear_order α] {f : α } {s : set α} (h : s) :
(p q : α ), s 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 lipschitz_on_with.comp_evariation_on_le {α : Type u_1} [linear_order α] {E : Type u_3} {F : Type u_4} {f : E F} {C : nnreal} {t : set E} (h : t) {g : α E} {s : set α} (hg : s t) :
theorem lipschitz_on_with.comp_has_bounded_variation_on {α : Type u_1} [linear_order α] {E : Type u_3} {F : Type u_4} {f : E F} {C : nnreal} {t : set E} (hf : t) {g : α E} {s : set α} (hg : s t) (h : s) :
s
theorem lipschitz_on_with.comp_has_locally_bounded_variation_on {α : Type u_1} [linear_order α] {E : Type u_3} {F : Type u_4} {f : E F} {C : nnreal} {t : set E} (hf : t) {g : α E} {s : set α} (hg : s t) (h : s) :
theorem lipschitz_with.comp_has_bounded_variation_on {α : Type u_1} [linear_order α] {E : Type u_3} {F : Type u_4} {f : E F} {C : nnreal} (hf : f) {g : α E} {s : set α} (h : s) :
s
theorem lipschitz_with.comp_has_locally_bounded_variation_on {α : Type u_1} [linear_order α] {E : Type u_3} {F : Type u_4} {f : E F} {C : nnreal} (hf : f) {g : α E} {s : set α} (h : s) :
theorem lipschitz_on_with.has_locally_bounded_variation_on {E : Type u_3} {f : E} {C : nnreal} {s : set } (hf : s) :
theorem lipschitz_with.has_locally_bounded_variation_on {E : Type u_3} {f : E} {C : nnreal} (hf : f) (s : set ) :

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

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

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

theorem has_locally_bounded_variation_on.ae_differentiable_within_at_of_mem {V : Type u_5} [ V] {f : V} {s : set } (h : s) :
∀ᵐ (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 has_locally_bounded_variation_on.ae_differentiable_within_at {V : Type u_5} [ V] {f : V} {s : set } (h : s) (hs : measurable_set s) :

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

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

theorem lipschitz_on_with.ae_differentiable_within_at_of_mem {V : Type u_5} [ V] {C : nnreal} {f : V} {s : set } (h : s) :
∀ᵐ (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 lipschitz_on_with.ae_differentiable_within_at {V : Type u_5} [ V] {C : nnreal} {f : V} {s : set } (h : s) (hs : measurable_set 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 lipschitz_with.ae_differentiable_at {V : Type u_5} [ V] {C : nnreal} {f : V} (h : f) :
∀ᵐ (x : ),

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