ae_differentiableAt — Mathlib

English

A monotone real function is almost everywhere differentiable with derivative given by rnDeriv of the Stieltjes measure.

Русский

Монотонная функция на R почти всюду дифференцируема, производная — радон-никодиевская производная меры Стилтьγεса.

LaTeX

$$$$ \forall f:\mathbb{R}\to\mathbb{R}, \text{Monotone}(f) \Rightarrow \text{ae differentiable} $$$$

Lean4

/-- A monotone real function is differentiable Lebesgue-almost everywhere. -/
theorem ae_differentiableAt {f : ℝ → ℝ} (hf : Monotone f) : ∀ᵐ x, DifferentiableAt ℝ f x := by
  filter_upwards [hf.ae_hasDerivAt] with x hx using hx.differentiableAt

Похожие утверждения