Theorems · Theorem · measure theory

MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasurableSet s →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
      Set.InjOn f s →
        MeasureTheory.Measure.map (s.domRestrict f)
            (MeasureTheory.Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) =
          μ.restrict (f '' s)

Change of variable formula for differentiable functions, set version: if a function f is injective and differentiable on a measurable set s, then the pushforward of the measure with density |(f' x).det| on s is the Lebesgue measure on the image set. This version is expressed in terms of the restricted function s.domRestrict f. For a version for the original function, see map_withDensity_abs_det_fderiv_eq_addHaar.

Defined in

Mathlib.MeasureTheory.Function.Jacobian

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddHaarMeasure