mathlib3 documentation

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 #

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} [pseudo_emetric_space E] (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} [pseudo_emetric_space E] (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} [pseudo_emetric_space 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

Basic computations of variation #

theorem evariation_on.nonempty_monotone_mem {α : Type u_1} [linear_order α] {s : set α} (hs : s.nonempty) :
nonempty {u // monotone u (i : ), u i s}
theorem evariation_on.eq_of_edist_zero_on {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] {f f' : α E} {s : set α} (h : ⦃x : α⦄, x s has_edist.edist (f x) (f' x) = 0) :
theorem evariation_on.eq_of_eq_on {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] {f f' : α E} {s : set α} (h : set.eq_on f f' s) :
theorem evariation_on.sum_le {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (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))) evariation_on f s
theorem evariation_on.sum_le_of_monotone_on_Iic {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (f : α E) {s : set α} {n : } {u : α} (hu : monotone_on u (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))) evariation_on f s
theorem evariation_on.sum_le_of_monotone_on_Icc {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (f : α E) {s : set α} {m n : } {u : α} (hu : monotone_on u (set.Icc m n)) (us : (i : ), i set.Icc m n u i s) :
(finset.Ico m n).sum (λ (i : ), has_edist.edist (f (u (i + 1))) (f (u i))) evariation_on f s
theorem evariation_on.mono {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (f : α E) {s t : set α} (hst : t s) :
theorem has_bounded_variation_on.mono {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] {f : α E} {s : set α} (h : has_bounded_variation_on f s) {t : set α} (ht : t s) :
theorem evariation_on.edist_le {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (f : α E) {s : set α} {x y : α} (hx : x s) (hy : y s) :
theorem evariation_on.eq_zero_iff {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (f : α E) {s : set α} :
evariation_on f s = 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} [pseudo_emetric_space E] {f : α E} {s : set α} (hf : (f '' s).subsingleton) :
@[protected, simp]
theorem evariation_on.subsingleton {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (f : α E) {s : set α} (hs : s.subsingleton) :
theorem evariation_on.lower_continuous_aux {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] {ι : 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 < evariation_on f s) :
∀ᶠ (n : ι) in p, v < evariation_on (F n) s
@[protected]

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.

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} [pseudo_metric_space E] {f : α E} {s : set α} (h : has_bounded_variation_on f s) {x y : α} (hx : x s) (hy : y s) :
theorem has_bounded_variation_on.sub_le {α : Type u_1} [linear_order α] {f : α } {s : set α} (h : has_bounded_variation_on f s) {x y : α} (hx : x s) (hy : y s) :
f x - f y (evariation_on f s).to_real
theorem evariation_on.add_point {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space 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 (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} [pseudo_emetric_space E] (f : α E) {s t : set α} (h : (x : α), x s (y : α), y t x 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 evariation_on.union {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (f : α E) {s t : set α} {x : α} (hs : is_greatest s x) (ht : is_least t x) :

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} [pseudo_emetric_space E] (f : α E) {s : set α} {a b c : α} (hab : a b) (hbc : b c) (hb : b s) :
theorem evariation_on.comp_le_of_monotone_on {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {E : Type u_3} [pseudo_emetric_space E] (f : α E) {s : set α} {t : set β} (φ : β α) (hφ : monotone_on φ t) (φst : set.maps_to φ t s) :
theorem evariation_on.comp_le_of_antitone_on {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {E : Type u_3} [pseudo_emetric_space E] (f : α E) {s : set α} {t : set β} (φ : β α) (hφ : antitone_on φ t) (φst : set.maps_to φ t s) :
theorem evariation_on.comp_eq_of_monotone_on {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {E : Type u_3} [pseudo_emetric_space E] (f : α E) {t : set β} (φ : β α) (hφ : monotone_on φ t) :
evariation_on (f φ) t = evariation_on f '' t)
theorem set.subsingleton_Icc_of_ge {α : Type u_1} [partial_order α] {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} [pseudo_emetric_space E] (f : α E) {t : set β} (φ : β α) (hφ : monotone_on φ t) {x y : β} (hx : x t) (hy : y t) :
evariation_on (f φ) (t set.Icc x y) = evariation_on f '' 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} [pseudo_emetric_space E] (f : α E) {t : set β} (φ : β α) (hφ : antitone_on φ t) :
evariation_on (f φ) t = evariation_on f '' t)

Monotone functions and bounded variation #

theorem monotone_on.evariation_on_le {α : Type u_1} [linear_order α] {f : α } {s : set α} (hf : monotone_on f s) {a b : α} (as : a s) (bs : b s) :
noncomputable def variation_on_from_to {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space 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
@[protected]
theorem variation_on_from_to.self {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (f : α E) (s : set α) (a : α) :
@[protected]
theorem variation_on_from_to.nonneg_of_le {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (f : α E) (s : set α) {a b : α} (h : a b) :
@[protected]
theorem variation_on_from_to.eq_neg_swap {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (f : α E) (s : set α) (a b : α) :
@[protected]
theorem variation_on_from_to.nonpos_of_ge {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (f : α E) (s : set α) {a b : α} (h : b a) :
@[protected]
theorem variation_on_from_to.eq_of_le {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (f : α E) (s : set α) {a b : α} (h : a b) :
@[protected]
theorem variation_on_from_to.eq_of_ge {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (f : α E) (s : set α) {a b : α} (h : b a) :
@[protected]
theorem variation_on_from_to.add {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] {f : α E} {s : set α} (hf : has_locally_bounded_variation_on f s) {a b c : α} (ha : a s) (hb : b s) (hc : c s) :
@[protected]
theorem variation_on_from_to.edist_zero_of_eq_zero {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] {f : α E} {s : set α} (hf : has_locally_bounded_variation_on f s) {a b : α} (ha : a s) (hb : b s) (h : variation_on_from_to f s 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} [pseudo_emetric_space E] {f : α E} {s : set α} (hf : has_locally_bounded_variation_on f s) {a b c : α} (ha : a s) (hb : b s) (hc : c s) :
@[protected]
theorem variation_on_from_to.eq_zero_iff_of_le {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] {f : α E} {s : set α} (hf : has_locally_bounded_variation_on f s) {a b : α} (ha : a s) (hb : b s) (ab : a b) :
variation_on_from_to f s a b = 0 ⦃x : α⦄, x s set.Icc a b ⦃y : α⦄, y s set.Icc a 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} [pseudo_emetric_space E] {f : α E} {s : set α} (hf : has_locally_bounded_variation_on f s) {a b : α} (ha : a s) (hb : b s) (ba : b a) :
variation_on_from_to f s a b = 0 ⦃x : α⦄, x s set.Icc b a ⦃y : α⦄, y s set.Icc b 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} [pseudo_emetric_space E] {f : α E} {s : set α} (hf : has_locally_bounded_variation_on f s) {a b : α} (ha : a s) (hb : b s) :
variation_on_from_to f s a b = 0 ⦃x : α⦄, x s set.uIcc a b ⦃y : α⦄, y s set.uIcc a 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} [pseudo_emetric_space E] {f : α E} {s : set α} (hf : has_locally_bounded_variation_on f s) {a : α} (as : a s) :
@[protected]
theorem variation_on_from_to.antitone_on {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] {f : α E} {s : set α} (hf : has_locally_bounded_variation_on f s) {b : α} (bs : b s) :
antitone_on (λ (a : α), variation_on_from_to f s a b) s
@[protected]
theorem variation_on_from_to.sub_self_monotone_on {α : Type u_1} [linear_order α] {f : α } {s : set α} (hf : has_locally_bounded_variation_on f s) {a : α} (as : a 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} [pseudo_emetric_space E] (f : α E) {t : set β} (φ : β α) (hφ : monotone_on φ t) {x y : β} (hx : x t) (hy : y t) :
variation_on_from_to (f φ) t x y = variation_on_from_to f '' t) (φ x) (φ y)

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} [pseudo_emetric_space E] [pseudo_emetric_space F] {f : E F} {C : nnreal} {t : set E} (h : lipschitz_on_with C f t) {g : α E} {s : set α} (hg : set.maps_to g s t) :
theorem lipschitz_on_with.comp_has_bounded_variation_on {α : Type u_1} [linear_order α] {E : Type u_3} {F : Type u_4} [pseudo_emetric_space E] [pseudo_emetric_space F] {f : E F} {C : nnreal} {t : set E} (hf : lipschitz_on_with C f t) {g : α E} {s : set α} (hg : set.maps_to g s t) (h : has_bounded_variation_on g s) :
theorem lipschitz_on_with.comp_has_locally_bounded_variation_on {α : Type u_1} [linear_order α] {E : Type u_3} {F : Type u_4} [pseudo_emetric_space E] [pseudo_emetric_space F] {f : E F} {C : nnreal} {t : set E} (hf : lipschitz_on_with C f t) {g : α E} {s : set α} (hg : set.maps_to g s t) (h : has_locally_bounded_variation_on g s) :
theorem lipschitz_with.comp_has_bounded_variation_on {α : Type u_1} [linear_order α] {E : Type u_3} {F : Type u_4} [pseudo_emetric_space E] [pseudo_emetric_space F] {f : E F} {C : nnreal} (hf : lipschitz_with C f) {g : α E} {s : set α} (h : has_bounded_variation_on g s) :

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.

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

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

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

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