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 spaces are also differentiable almost everywhere.

Main definitions and results

• LocallyBoundedVariationOn.ae_differentiableWithinAt shows that a bounded variation function on a subset of ℝ into a finite-dimensional real vector space is differentiable almost everywhere, with DifferentiableWithinAt in its conclusion.
• BoundedVariationOn.ae_differentiableAt_of_mem_uIcc shows that a bounded variation function on an interval of ℝ into a finite-dimensional real vector space is differentiable almost everywhere, with DifferentiableAt in its conclusion.
• LipschitzOnWith.ae_differentiableWithinAt is the same result for Lipschitz functions.

We also give several variations around these results.

theorem eVariationOn_bilinear_comp_le {α : Type u_2} [LinearOrder α] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {s : Set α} {f : α → E} {g : α → F} {C D : ENNReal} (hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C) (hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D) (B : E →L[ℝ] F →L[ℝ] G) : eVariationOn (fun (x : α) => (B (f x)) (g x)) s ≤ ‖B‖ₑ * (C * eVariationOn g s + D * eVariationOn f s)

theorem eVariationOn_smul_le {α : Type u_2} [LinearOrder α] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {𝕜 : Type u_6} {f : α → 𝕜} {g : α → F} [NormedRing 𝕜] [NormedAlgebra ℝ 𝕜] [Module 𝕜 F] [NormSMulClass 𝕜 F] [IsScalarTower ℝ 𝕜 F] {C D : ENNReal} {s : Set α} (hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C) (hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D) : eVariationOn (f • g) s ≤ C * eVariationOn g s + D * eVariationOn f s

theorem eVariationOn_fun_smul_le {α : Type u_2} [LinearOrder α] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {𝕜 : Type u_6} {f : α → 𝕜} {g : α → F} [NormedRing 𝕜] [NormedAlgebra ℝ 𝕜] [Module 𝕜 F] [NormSMulClass 𝕜 F] [IsScalarTower ℝ 𝕜 F] {C D : ENNReal} {s : Set α} (hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C) (hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D) : eVariationOn (fun (i : α) => f i • g i) s ≤ C * eVariationOn g s + D * eVariationOn f s

Eta-expanded form of eVariationOn_smul_le

theorem eVariation_mul_le {α : Type u_2} [LinearOrder α] {f g : α → ℝ} {C D : ENNReal} {s : Set α} (hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C) (hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D) : eVariationOn (f * g) s ≤ C * eVariationOn g s + D * eVariationOn f s

theorem eVariationOn_fun_mul_le {α : Type u_2} [LinearOrder α] {f g : α → ℝ} {C D : ENNReal} {s : Set α} (hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C) (hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D) : eVariationOn (fun (i : α) => f i * g i) s ≤ C * eVariationOn g s + D * eVariationOn f s

Eta-expanded form of eVariation_mul_le

theorem BoundedVariationOn.bilinear_comp {α : Type u_2} [LinearOrder α] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {s : Set α} {f : α → E} {g : α → F} (hf : BoundedVariationOn f s) (hg : BoundedVariationOn g s) (B : E →L[ℝ] F →L[ℝ] G) : BoundedVariationOn (fun (x : α) => (B (f x)) (g x)) s

theorem BoundedVariationOn.smul {α : Type u_2} [LinearOrder α] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {𝕜 : Type u_6} {f : α → 𝕜} {g : α → F} [NormedRing 𝕜] [NormedAlgebra ℝ 𝕜] [Module 𝕜 F] [NormSMulClass 𝕜 F] [IsScalarTower ℝ 𝕜 F] {s : Set α} (hf : BoundedVariationOn f s) (hg : BoundedVariationOn g s) : BoundedVariationOn (f • g) s

theorem BoundedVariationOn.fun_smul {α : Type u_2} [LinearOrder α] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {𝕜 : Type u_6} {f : α → 𝕜} {g : α → F} [NormedRing 𝕜] [NormedAlgebra ℝ 𝕜] [Module 𝕜 F] [NormSMulClass 𝕜 F] [IsScalarTower ℝ 𝕜 F] {s : Set α} (hf : BoundedVariationOn f s) (hg : BoundedVariationOn g s) : BoundedVariationOn (fun (i : α) => f i • g i) s

Eta-expanded form of BoundedVariationOn.smul

theorem BoundedVariationOn.mul {α : Type u_2} [LinearOrder α] {f g : α → ℝ} {s : Set α} (hf : BoundedVariationOn f s) (hg : BoundedVariationOn g s) : BoundedVariationOn (f * g) s

theorem BoundedVariationOn.fun_mul {α : Type u_2} [LinearOrder α] {f g : α → ℝ} {s : Set α} (hf : BoundedVariationOn f s) (hg : BoundedVariationOn g s) : BoundedVariationOn (fun (i : α) => f i * g i) s

Eta-expanded form of BoundedVariationOn.mul

theorem LocallyBoundedVariationOn.bilinear_comp {α : Type u_2} [LinearOrder α] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {s : Set α} {f : α → E} {g : α → F} (hf : LocallyBoundedVariationOn f s) (hg : LocallyBoundedVariationOn g s) (B : E →L[ℝ] F →L[ℝ] G) : LocallyBoundedVariationOn (fun (x : α) => (B (f x)) (g x)) s

theorem LocallyBoundedVariationOn.smul {α : Type u_2} [LinearOrder α] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {𝕜 : Type u_6} {f : α → 𝕜} {g : α → F} [NormedRing 𝕜] [NormedAlgebra ℝ 𝕜] [Module 𝕜 F] [NormSMulClass 𝕜 F] [IsScalarTower ℝ 𝕜 F] {s : Set α} (hf : LocallyBoundedVariationOn f s) (hg : LocallyBoundedVariationOn g s) : LocallyBoundedVariationOn (f • g) s

theorem LocallyBoundedVariationOn.fun_smul {α : Type u_2} [LinearOrder α] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {𝕜 : Type u_6} {f : α → 𝕜} {g : α → F} [NormedRing 𝕜] [NormedAlgebra ℝ 𝕜] [Module 𝕜 F] [NormSMulClass 𝕜 F] [IsScalarTower ℝ 𝕜 F] {s : Set α} (hf : LocallyBoundedVariationOn f s) (hg : LocallyBoundedVariationOn g s) : LocallyBoundedVariationOn (fun (i : α) => f i • g i) s

Eta-expanded form of LocallyBoundedVariationOn.smul

theorem LocallyBoundedVariationOn.mul {α : Type u_2} [LinearOrder α] {f g : α → ℝ} {s : Set α} (hf : LocallyBoundedVariationOn f s) (hg : LocallyBoundedVariationOn g s) : LocallyBoundedVariationOn (f * g) s

theorem LocallyBoundedVariationOn.fun_mul {α : Type u_2} [LinearOrder α] {f g : α → ℝ} {s : Set α} (hf : LocallyBoundedVariationOn f s) (hg : LocallyBoundedVariationOn g s) : LocallyBoundedVariationOn (fun (i : α) => f i * g i) s

Eta-expanded form of LocallyBoundedVariationOn.mul

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_2} [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_1} [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 BoundedVariationOn.ae_differentiableAt_of_mem_uIcc {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {f : ℝ → V} {a b : ℝ} (h : BoundedVariationOn f (Set.uIcc a b)) : ∀ᵐ (x : ℝ), x ∈ Set.uIcc a b → DifferentiableAt ℝ f x

A real function into a finite-dimensional real vector space with bounded variation on an interval is differentiable almost everywhere in this interval. This one differs from LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem by using DifferentiableAt instead of DifferentiableWithinAt in its conclusion.

theorem LocallyBoundedVariationOn.ae_differentiableWithinAt {V : Type u_1} [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_1} [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_1} [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_1} [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_1} [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.