lintegral_deriv_eq_volume_image_of_antitoneOn

English

If f is antitone, the image change of variables holds with |f'| replaced by |-f'|, which equals |f'|.

Русский

Если f антиинвариантна, формула замены переменной по образу сохраняется, так как |-f'| = |f'|.

LaTeX

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

Lean4

/-- Change of variable formula for differentiable functions, set version: if a real function `f` is
antitone and differentiable on a measurable set `s`, then the measure of `f '' s` is given by the
integral of `-f' x` on `s` .
Note that the measurability of `f '' s` is given by `MeasurableSet.image_of_antitoneOn`. -/
theorem lintegral_deriv_eq_volume_image_of_antitoneOn (hs : MeasurableSet s)
    (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : AntitoneOn f s) :
    (∫⁻ x in s, ENNReal.ofReal (-f' x)) = volume (f '' s) := by
  simpa using (lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn hs hf' hf 1).symm

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