Theorems · Theorem · measure theory

MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure],
  MeasurableSet s →
    ∀ (f : E ≃ᵐ E) {g : E → ℝ},
      (∀ᵐ (x : E) ∂μ, x ∈ ⇑f '' s → 0 ≤ g x) →
        MeasureTheory.IntegrableOn g (⇑f '' s) μ →
          (∀ x ∈ s, HasFDerivWithinAt (⇑f) (f' x) s x) →
            (MeasureTheory.Measure.map (⇑f.symm) (μ.withDensity fun x => ENNReal.ofReal (g x))) s =
              ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)

Defined in

Mathlib.MeasureTheory.Function.Jacobian

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddHaarMeasure