Theorems · Theorem · measure theory

MeasureTheory.integral_image_eq_integral_deriv_smul_of_monotoneOn

∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
      MonotoneOn f s → ∀ (g : ℝ → F), ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, f' x • g (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 Bochner integral of a function g : ℝ → F on f '' s coincides with the integral of (f' x) • g ∘ f on s .

Defined in

Mathlib.MeasureTheory.Function.JacobianOneDim

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace