withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul

English

The image integration with a function g over f''s equals the integral over s of |det f'| times g∘f.

Русский

Интеграл по образу f''s функции g равен интегралу по s от |det f'| · g(f(x)).

LaTeX

$$$$ \\int_{f''s} g(x) \\, d\\mu = \\int_s |\\det f'(x)| \\cdot g(f(x)) \\, d\\mu $$$$

Lean4

theorem _root_.MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul (hs : MeasurableSet s)
    (hf : MeasurableEmbedding f) {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))).comap f s = ENNReal.ofReal (∫ x in s, |(f' x).det| * g (f x) ∂μ) :=
  by
  rw [Measure.comap_apply f hf.injective (fun t ht ↦ hf.measurableSet_image' ht) _ hs,
    withDensity_apply _ (hf.measurableSet_image' hs), ←
    ofReal_integral_eq_lintegral_ofReal hg_int ((ae_restrict_iff' (hf.measurableSet_image' hs)).mpr hg),
    integral_image_eq_integral_abs_det_fderiv_smul μ hs hf' hf.injective.injOn]
  simp_rw [smul_eq_mul]

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