English
One-dimensional version: for differentiable f on a measurable s ⊆ R, ∫_{f''s} g = ∫_s |f'| g∘f with appropriate orientation.
Русский
Одномерная версия: если f дифференцируема на измеримом s ⊆ R, то ∫_{f''s} g = ∫_s |f'| g∘f с учётом ориентации.
LaTeX
$$$$ \\int_{f''s} g(x) dx = \\int_s |f'(x)| \\cdot g(f(x)) dx $$$$
Lean4
/-- Change of variable formula for differentiable functions: if a real function `f` is
antitone and differentiable on a measurable set `s`, then the Bochner integral of a function
`g : ℝ → F` on `f '' s` coincides with the integral of `(-f' x) • g ∘ f` on `s` . -/
theorem integral_image_eq_integral_deriv_smul_of_antitone (hs : MeasurableSet s)
(hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : AntitoneOn f s) (g : ℝ → F) :
∫ x in f '' s, g x = ∫ x in s, (-f' x) • g (f x) :=
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 : ∫ x in e '' s, g (n x) = ∫ x in s, (-f' x) • (g ∘ n) (e x) := by
rw [← integral_image_eq_integral_deriv_smul_of_monotoneOn hs hg' hf.neg (g ∘ n)]; rfl
have B : ∫ x in n '' (e '' s), g x = ∫ x in e '' s, (|-1| : ℝ) • g (n x) :=
integral_image_eq_integral_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]
