Almost everywhere differentiability of functions with locally bounded variation

In this file we show that a bounded variation function is 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

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

theorem LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_real {f : ℝ → ℝ} {s : Set ℝ} (h : LocallyBoundedVariationOn f s) : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

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} [Fintype ι] {f : ℝ → ι → ℝ} {s : Set ℝ} (h : LocallyBoundedVariationOn f s) : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

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} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {f : ℝ → V} {s : Set ℝ} (h : LocallyBoundedVariationOn f s) : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ 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 LocallyBoundedVariationOn.ae_differentiableWithinAt {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {f : ℝ → V} {s : Set ℝ} (h : LocallyBoundedVariationOn f s) (hs : MeasurableSet s) : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt ℝ 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 LocallyBoundedVariationOn.ae_differentiableAt {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {f : ℝ → V} (h : LocallyBoundedVariationOn f Set.univ) : ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x

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

theorem LipschitzOnWith.ae_differentiableWithinAt_of_mem_real {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {C : NNReal} {f : ℝ → V} {s : Set ℝ} (h : LipschitzOnWith C f s) : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ 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. For the general Rademacher theorem assuming that the source space is finite dimensional, see LipschitzOnWith.ae_differentiableWithinAt_of_mem.

theorem LipschitzOnWith.ae_differentiableWithinAt_real {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {C : NNReal} {f : ℝ → V} {s : Set ℝ} (h : LipschitzOnWith C f s) (hs : MeasurableSet s) : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt ℝ 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. For the general Rademacher theorem assuming that the source space is finite dimensional, see LipschitzOnWith.ae_differentiableWithinAt.

theorem LipschitzWith.ae_differentiableAt_real {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {C : NNReal} {f : ℝ → V} (h : LipschitzWith C f) : ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x

A real Lipschitz function into a finite dimensional real vector space is differentiable almost everywhere. For the general Rademacher theorem assuming that the source space is finite dimensional, see LipschitzWith.ae_differentiableAt.