English
For a finite index set, a LocallyBoundedVariationOn f s implies differentiability almost everywhere in s componentwise.
Русский
Для конечного множества индексов LocallyBoundedVariationOn f s обеспечивает асимптотическую дифференцируемость по компонентам в s.
LaTeX
$$$\forall \iota:\; [Fintype \iota] \; f:\mathbb{R} \to (\iota \to \mathbb{R})\; (h: LocallyBoundedVariationOn f s)\Rightarrow \forall i, DifferentiableWithinAt \mathbb{R} (\lambda x. f x i) s x$$$
Lean4
/-- A bounded variation function into `ℝ` is differentiable almost everywhere. Superseded by
`ae_differentiableWithinAt_of_mem`. -/
theorem ae_differentiableWithinAt_of_mem_real {f : ℝ → ℝ} {s : Set ℝ} (h : LocallyBoundedVariationOn f s) :
∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ f s x :=
by
obtain ⟨p, q, hp, hq, rfl⟩ : ∃ p q, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q := h.exists_monotoneOn_sub_monotoneOn
filter_upwards [hp.ae_differentiableWithinAt_of_mem, hq.ae_differentiableWithinAt_of_mem] with x hxp hxq xs
exact (hxp xs).sub (hxq xs)
