English
In the antitone case, the change of variables formula uses -f' in the density: the image measure equals the restricted integral with density |-f'|.
Русский
В случае антиинвариантности замена переменной использует -f' в плотности: образующая мера равна интегралу по ограниченному множеству с плотностью |-f'|.
LaTeX
$$$$ \\int_{f''s} g(x) dx = \\int_s |-f'(x)| \\cdot g(f(x)) dx $$$$
Lean4
/-- Integrability in the change of variable formula for differentiable functions: if a real
function `f` is antitone and differentiable on a measurable set `s`, then a function
`g : ℝ → F` is integrable on `f '' s` if and only if `-f' x • g ∘ f` is integrable on `s` . -/
theorem integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOn (hs : MeasurableSet s)
(hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : AntitoneOn f s) (g : ℝ → F) :
IntegrableOn g (f '' s) ↔ IntegrableOn (fun x ↦ (-f' x) • g (f x)) s :=
by
let n : ℝ → ℝ := (fun x ↦ -x)
let e := n ∘ f
have hg' (x) (hx : x ∈ s) : HasDerivWithinAt e (-f' x) s x := (hf' x hx).neg
have A : IntegrableOn (fun x ↦ g (n x)) (e '' s) ↔ IntegrableOn (fun x ↦ (-f' x) • (g ∘ n) (e x)) s := by
rw [← integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn hs hg' hf.neg (g ∘ n)]; rfl
have B : IntegrableOn g (n '' (e '' s)) ↔ IntegrableOn (fun x ↦ (|-1| : ℝ) • g (n x)) (e '' s) :=
integrableOn_image_iff_integrableOn_abs_deriv_smul (hs.image_of_monotoneOn hf.neg)
(fun x hx ↦ hasDerivWithinAt_neg _ _) neg_injective.injOn _
simp only [abs_neg, abs_one, one_smul] at B
rw [A, ← image_comp] at B
convert B using 3 with x hx x <;> simp [n, e]
