withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul'

English

For an antitone differentiable map on s, the general derivative-based image formula holds with the minus derivative in the integrand.

Русский

Для антиинвариантной отображения на s общая формула изображения через производную выполняется с минусом производной в интегране.

LaTeX

$$$$ \\int_{f''s} g(x) dx = \\int_s (-f'(x)) \\cdot g(f(x)) dx $$$$

Lean4

theorem _root_.MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul' (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))).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
      (by filter_upwards [hg] with x hx using fun _ ↦ hx) hg_int.integrableOn (fun x _ => (hf' x).hasDerivWithinAt)]
  simp only [det_one_smulRight]

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