Theorems · Theorem · real analysis

BoundedVariationOn.ae_differentiableAt_of_mem_uIcc

∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [FiniteDimensional ℝ V] {f : ℝ → V} {a b : ℝ},
  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.

Defined in

Mathlib.Analysis.BoundedVariation

Cited by

1 results in Mathlib

Foundations

Depth 269 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensional