Theorems · Theorem · measure theory

MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn

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

Change of variable formula for differentiable functions: if a real function f is monotone and differentiable on a measurable set s, then the Lebesgue integral of a function u : ℝ → ℝ≥0∞ on f '' s coincides with the integral of (f' x) * u ∘ f on s. Note that the measurability of f '' s is given by MeasurableSet.image_of_monotoneOn.

Defined in

Mathlib.MeasureTheory.Function.JacobianOneDim

Cited by

3 results in Mathlib

Foundations

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