Theorems · Theorem · measure theory

MeasureTheory.lintegral_deriv_eq_volume_image_of_monotoneOn

∀ {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
      MonotoneOn f s → ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) = MeasureTheory.volume (f '' s)

Change of variable formula for differentiable functions, set version: if a real function f is monotone and differentiable on a measurable set s, then the measure of f '' s is given by the integral of f' x on s . Note that the measurability of f '' s is given by MeasurableSet.image_of_monotoneOn.

Defined in

Mathlib.MeasureTheory.Function.JacobianOneDim

Cited by

0 results in Mathlib

Foundations

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