withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul'

English

Given a measurable equivalence, the pushforward of the density through the equivalence equals the density on the image.

Русский

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

LaTeX

$$$$ \\mathrm{withDensity}(g) \\mapsto \\mathrm{map}(f) = \\int g $$$$

Lean4

theorem _root_.MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul' {f : ℝ → ℝ}
    (hf : MeasurableEmbedding f) {s : Set ℝ} (hs : MeasurableSet s) {f' : ℝ → ℝ} (hf' : ∀ x, HasDerivAt f (f' x) x)
    {g : ℝ → ℝ} (hg : 0 ≤ᵐ[volume] g) (hg_int : Integrable g) :
    (volume.withDensity (fun x ↦ ENNReal.ofReal (g x))).comap f s = ENNReal.ofReal (∫ x in s, |f' x| * g (f x)) :=
  hf.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul hs (by filter_upwards [hg] with x hx using fun _ ↦ hx)
    hg_int.integrableOn (fun x _ => (hf' x).hasDerivWithinAt)

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