withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul

English

Under a measurable embedding, the comapped with density density identity holds for the image measure.

Русский

При измеримой вложенности равенство переноса через плотность и перенос по образу меры сохраняется.

LaTeX

$$$$ \\mathrm{withDensity}(g) \\mapsto \\mathrm{comap}(f)(\\mathrm{volume} \\text{ withDensity } g) = \\int g $$$$

Lean4

theorem _root_.MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul (f : ℝ ≃ᵐ ℝ) {s : Set ℝ}
    (hs : MeasurableSet s) {g : ℝ → ℝ} (hg : ∀ᵐ x, x ∈ f '' s → 0 ≤ g x) (hf_int : IntegrableOn g (f '' s)) {f' : ℝ → ℝ}
    (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) :
    (volume.withDensity (fun x ↦ ENNReal.ofReal (g x))).map f.symm s = ENNReal.ofReal (∫ x in s, |f' x| * g (f x)) :=
  by
  rw [MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul volume hs f hg hf_int hf']
  simp only [det_one_smulRight]

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