English
For a differentiable map f with appropriate domain and target, the integral of g over the target equals the integral over the source of |det f'| · g∘f.
Русский
Для дифференцируемого отображения f с подходящими доменом и целевой областью интеграл по образу равен интегралу по источнику от |det f'|·g∘f.
LaTeX
$$$$ \\int_{\\mathrm{target}} g(x) \\, d\\mu = \\int_{\\mathrm{source}} |\\det f'(x)| \\cdot g(f(x)) \\, d\\mu $$$$
Lean4
theorem lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn (hs : MeasurableSet s)
(hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : AntitoneOn f s) (u : ℝ → ℝ≥0∞) :
∫⁻ x in f '' s, u x = ∫⁻ x in s, ENNReal.ofReal (-f' x) * u (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, u (n x) = ∫⁻ x in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x) := by
rw [← lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn hs hg' hf.neg (u ∘ n)]; rfl
have B : ∫⁻ x in n '' (e '' s), u x = ∫⁻ x in e '' s, ENNReal.ofReal (|-1|) * u (n x) :=
lintegral_image_eq_lintegral_abs_deriv_mul (hs.image_of_monotoneOn hf.neg) (fun x hx ↦ hasDerivWithinAt_neg _ _)
neg_injective.injOn _
simp only [abs_neg, abs_one, ENNReal.ofReal_one, one_mul] at B
rw [A, ← image_comp] at B
convert B using 4 with x hx x <;> simp [n, e]
