Theorems · Theorem · measure theory

MeasureTheory.integrableOn_image_iff_integrableOn_abs_deriv_smul

∀ {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) →
      Set.InjOn f s →
        ∀ (g : ℝ → F),
          MeasureTheory.IntegrableOn g (f '' s) MeasureTheory.volume ↔
            MeasureTheory.IntegrableOn (fun x => |f' x| • g (f x)) s MeasureTheory.volume

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 a function g : ℝ → F is integrable on f '' s if and only if |(f' x)| • g ∘ f is integrable on s.

Defined in

Mathlib.MeasureTheory.Function.JacobianOneDim

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace