withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul

English

Under a measurable bijection, the pushforward with density coincides with the same density transported to the image set.

Русский

При измеримой биекции переходная мера с плотностью совпадает с плотностью, перенесенной на образ этого множества.

LaTeX

$$$$ \\mathrm{map}(\\text{f})((\\mu|_s)\\mathrm{withDensity}(|\\det f'|)) = \\mu|_{f''s} $$$$

Lean4

theorem _root_.MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul (hs : MeasurableSet s)
    (f : E ≃ᵐ E) {g : E → ℝ} (hg : ∀ᵐ x ∂μ, x ∈ f '' s → 0 ≤ g x) (hg_int : IntegrableOn g (f '' s) μ)
    (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :
    (μ.withDensity (fun x ↦ ENNReal.ofReal (g x))).map f.symm s =
      ENNReal.ofReal (∫ x in s, |(f' x).det| * g (f x) ∂μ) :=
  by
  rw [MeasurableEquiv.map_symm,
    MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul μ hs f.measurableEmbedding hg
      hg_int hf']

Похожие утверждения