Theorems · Theorem · measure theory

MeasureTheory.lintegral_image_eq_lintegral_abs_deriv_mul

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

Integrability in the change of variable formula for differentiable functions (one-variable version): if a function f is injective and differentiable on a measurable set s ⊆ ℝ, then the Lebesgue integral of a function g : ℝ → ℝ≥0∞ on f '' s coincides with the Lebesgue integral of |(f' x)| * g ∘ f on s.

Defined in

Mathlib.MeasureTheory.Function.JacobianOneDim

Cited by

1 results in Mathlib

Foundations

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