Theorems · Theorem · measure theory

MeasureTheory.integrableOn_image_iff_integrableOn_abs_det_fderiv_smul

∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E}
  [inst_5 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure],
  MeasurableSet s →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
      Set.InjOn f s →
        ∀ (g : E → F),
          MeasureTheory.IntegrableOn g (f '' s) μ ↔ MeasureTheory.IntegrableOn (fun x => |(f' x).det| • g (f x)) s μ

Integrability in the change of variable formula for differentiable functions: if a function f is injective and differentiable on a measurable set s, then a function g : E → F is integrable on f '' s if and only if |(f' x).det| • g ∘ f is integrable on s.

Defined in

Mathlib.MeasureTheory.Function.Jacobian

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalNormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddHaarMeasure