withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul

English

For a measurable equivalence, the density-adjusted image integral matches the pulled-back integral under the inverse map.

Русский

Для измеримой эквивалентности интеграл с плотностью совпадает с обратной индукцией интеграла через обратную карту.

LaTeX

$$$$ \\int g = \\int (|f'|) g(f) $$$$

Lean4

theorem _root_.MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul {f : ℝ → ℝ}
    (hf : MeasurableEmbedding 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))).comap f s = ENNReal.ofReal (∫ x in s, |f' x| * g (f x)) :=
  by
  rw [hf.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul volume hs hg hf_int hf']
  simp only [det_one_smulRight]

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