English
For a finite dimensional target, a LocallyBoundedVariationOn f s yields differentiability almost everywhere on s.
Русский
Для конечномерной цели LocallyBoundedVariationOn f s обеспечивает дифференцируемость почти повсюду на s.
LaTeX
$$$\forall f:\mathbb{R}^n \to \mathbb{R}^m,\; h: LocallyBoundedVariationOn f s \Rightarrow \ae x\in volume.restrict s, DifferentiableWithinAt \mathbb{R} f s x$$$
Lean4
/-- A real function into a finite-dimensional real vector space with bounded variation on a set
is differentiable almost everywhere in this set. -/
theorem ae_differentiableWithinAt_of_mem {f : ℝ → V} {s : Set ℝ} (h : LocallyBoundedVariationOn f s) :
∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ f s x :=
by
let A := (Module.Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
suffices H : ∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ (A ∘ f) s x
by
filter_upwards [H] with x hx xs
have : f = (A.symm ∘ A) ∘ f := by simp only [ContinuousLinearEquiv.symm_comp_self, Function.id_comp]
rw [this]
exact A.symm.differentiableAt.comp_differentiableWithinAt x (hx xs)
apply ae_differentiableWithinAt_of_mem_pi
exact A.lipschitz.comp_locallyBoundedVariationOn h
