English
A measurable set s and LocallyBoundedVariationOn f s imply almost everywhere differentiability of f componentwise on s.
Русский
Для множества s с измеримости и LocallyBoundedVariationOn f s дифференцируемость f по компонентам почти повсюду на s.
LaTeX
$$$\forall \iota [Fintype], f:\mathbb{R} \to (\iota \to \mathbb{R})\; (h: LocallyBoundedVariationOn f s)\Rightarrow \ae x\in volume.restrict s, DifferentiableWithinAt \mathbb{R} f s x$$$
Lean4
/-- A bounded variation function into a finite-dimensional product vector space is differentiable
almost everywhere. Superseded by `ae_differentiableWithinAt_of_mem`. -/
theorem ae_differentiableWithinAt_of_mem_pi {ι : Type*} [Fintype ι] {f : ℝ → ι → ℝ} {s : Set ℝ}
(h : LocallyBoundedVariationOn f s) : ∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ f s x :=
by
have A : ∀ i : ι, LipschitzWith 1 fun x : ι → ℝ => x i := fun i => LipschitzWith.eval i
have : ∀ i : ι, ∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ (fun x : ℝ => f x i) s x := fun i ↦
by
apply ae_differentiableWithinAt_of_mem_real
exact LipschitzWith.comp_locallyBoundedVariationOn (A i) h
filter_upwards [ae_all_iff.2 this] with x hx xs
exact differentiableWithinAt_pi.2 fun i => hx i xs
