Theorems · Theorem · measure theory

MeasureTheory.aemeasurable_fderivWithin

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure], MeasurableSet s → (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → AEMeasurable f' (μ.restrict s)

The derivative of a function on a measurable set is almost everywhere measurable on this set with respect to Lebesgue measure. Note that, in general, it is not genuinely measurable there, as f' is not unique (but only on a set of measure 0, as the argument shows).

Defined in

Mathlib.MeasureTheory.Function.Jacobian

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddHaarMeasure