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 #

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} [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

evariation_on f s = ⨆ (p : ℕ × {u // monotone u ∧ ∀ (i : ℕ), u i ∈ s}), (finset.range p.fst).sum (λ (i : ℕ), has_edist.edist (f (↑(p.snd) (i + 1))) (f (↑(p.snd) i)))

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

has_bounded_variation_on f s = (evariation_on f s ≠ ⊤)

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

has_locally_bounded_variation_on f s = ∀ (a b : α), a ∈ s → b ∈ s → has_bounded_variation_on f (s ∩ set.Icc a b)

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

evariation_on f s = evariation_on f' s

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

evariation_on f s = evariation_on 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) :

evariation_on f t ≤ evariation_on f 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) :

has_bounded_variation_on f t

theorem has_bounded_variation_on.has_locally_bounded_variation_on {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] {f : α → E} {s : set α} (h : has_bounded_variation_on f s) :

has_locally_bounded_variation_on f 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) :

has_edist.edist (f x) (f y) ≤ evariation_on f 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) :

evariation_on f s = 0

@[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) :

evariation_on f s = 0

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]

theorem evariation_on.lower_semicontinuous {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (s : set α) :

lower_semicontinuous (λ (f : uniform_on_fun α E (has_singleton.singleton '' s)), evariation_on 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} [pseudo_emetric_space E] (s : set α) :

lower_semicontinuous (λ (f : uniform_on_fun α E {s}), evariation_on f 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) :

has_dist.dist (f x) (f y) ≤ (evariation_on f s).to_real

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

evariation_on f s + evariation_on f t ≤ evariation_on 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 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) :

evariation_on f (s ∪ t) = evariation_on f s + evariation_on 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 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) :

evariation_on f (s ∩ set.Icc a b) + evariation_on f (s ∩ set.Icc b c) = evariation_on f (s ∩ set.Icc a c)

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

evariation_on (f ∘ φ) t ≤ evariation_on f 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) :

evariation_on (f ∘ φ) t ≤ evariation_on f 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) :

(set.Icc a b).subsingleton

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)

theorem evariation_on.comp_of_dual {α : Type u_1} [linear_order α] {E : Type u_3} [pseudo_emetric_space E] (f : α → E) (s : set α) :

evariation_on (f ∘ ⇑order_dual.of_dual) (⇑order_dual.of_dual ⁻¹' s) = evariation_on f s

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

evariation_on f (s ∩ set.Icc a 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 : monotone_on f s) :

has_locally_bounded_variation_on f 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

variation_on_from_to f s a b = ite (a ≤ b) (evariation_on f (s ∩ set.Icc a b)).to_real (-(evariation_on f (s ∩ set.Icc b a)).to_real)

@[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 : α) :

variation_on_from_to f s a a = 0

@[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) :

0 ≤ variation_on_from_to f s 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 : α) :

variation_on_from_to f s a b = -variation_on_from_to f s b a

@[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) :

variation_on_from_to f s a b ≤ 0

@[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) :

variation_on_from_to f s a b = (evariation_on f (s ∩ set.Icc a b)).to_real

@[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) :

variation_on_from_to f s a b = -(evariation_on f (s ∩ set.Icc b a)).to_real

@[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) :

variation_on_from_to f s a b + variation_on_from_to f s b c = variation_on_from_to f s a c

@[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) :

variation_on_from_to f s a b = variation_on_from_to f s a c ↔ variation_on_from_to f s b c = 0

@[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) :

monotone_on (variation_on_from_to f s 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) :

monotone_on (variation_on_from_to f s 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} [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)

theorem has_locally_bounded_variation_on.exists_monotone_on_sub_monotone_on {α : Type u_1} [linear_order α] {f : α → ℝ} {s : set α} (h : has_locally_bounded_variation_on f s) :

∃ (p q : α → ℝ), monotone_on p s ∧ monotone_on 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 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) :

evariation_on (f ∘ g) s ≤ ↑C * evariation_on g s

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

has_bounded_variation_on (f ∘ 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) :

has_locally_bounded_variation_on (f ∘ 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) :

has_bounded_variation_on (f ∘ g) s

theorem lipschitz_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} (hf : lipschitz_with C f) {g : α → E} {s : set α} (h : has_locally_bounded_variation_on g s) :

has_locally_bounded_variation_on (f ∘ g) s

theorem lipschitz_on_with.has_locally_bounded_variation_on {E : Type u_3} [pseudo_emetric_space E] {f : ℝ → E} {C : nnreal} {s : set ℝ} (hf : lipschitz_on_with C f s) :

has_locally_bounded_variation_on f s

theorem lipschitz_with.has_locally_bounded_variation_on {E : Type u_3} [pseudo_emetric_space E] {f : ℝ → E} {C : nnreal} (hf : lipschitz_with C f) (s : set ℝ) :

has_locally_bounded_variation_on f s

Almost everywhere differentiability of functions with locally bounded variation #

theorem has_locally_bounded_variation_on.ae_differentiable_within_at_of_mem_real {f : ℝ → ℝ} {s : set ℝ} (h : has_locally_bounded_variation_on f s) :

∀ᵐ (x : ℝ), x ∈ s → differentiable_within_at ℝ f s x

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

theorem has_locally_bounded_variation_on.ae_differentiable_within_at_of_mem_pi {ι : Type u_1} [fintype ι] {f : ℝ → ι → ℝ} {s : set ℝ} (h : has_locally_bounded_variation_on f s) :

∀ᵐ (x : ℝ), x ∈ s → differentiable_within_at ℝ f s x

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} [normed_add_comm_group V] [normed_space ℝ V] [finite_dimensional ℝ V] {f : ℝ → V} {s : set ℝ} (h : has_locally_bounded_variation_on f s) :

∀ᵐ (x : ℝ), x ∈ s → differentiable_within_at ℝ f s x

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} [normed_add_comm_group V] [normed_space ℝ V] [finite_dimensional ℝ V] {f : ℝ → V} {s : set ℝ} (h : has_locally_bounded_variation_on f s) (hs : measurable_set s) :

∀ᵐ (x : ℝ) ∂measure_theory.measure_space.volume.restrict s, differentiable_within_at ℝ f s x

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_at {V : Type u_5} [normed_add_comm_group V] [normed_space ℝ V] [finite_dimensional ℝ V] {f : ℝ → V} (h : has_locally_bounded_variation_on f set.univ) :

∀ᵐ (x : ℝ), differentiable_at ℝ f x

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} [normed_add_comm_group V] [normed_space ℝ V] [finite_dimensional ℝ V] {C : nnreal} {f : ℝ → V} {s : set ℝ} (h : lipschitz_on_with C f s) :

∀ᵐ (x : ℝ), x ∈ s → differentiable_within_at ℝ f s x

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} [normed_add_comm_group V] [normed_space ℝ V] [finite_dimensional ℝ V] {C : nnreal} {f : ℝ → V} {s : set ℝ} (h : lipschitz_on_with C f s) (hs : measurable_set s) :

∀ᵐ (x : ℝ) ∂measure_theory.measure_space.volume.restrict s, differentiable_within_at ℝ f s x

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} [normed_add_comm_group V] [normed_space ℝ V] [finite_dimensional ℝ V] {C : nnreal} {f : ℝ → V} (h : lipschitz_with C f) :

∀ᵐ (x : ℝ), differentiable_at ℝ f x

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