integral_comp_rpow_Ioi_of_pos — Mathlib

English

If p > 0, then the same substitution formula holds without the absolute value in the Jacobian factor: ∫_{Ioi 0} p x^{p-1} g(x^p) dx = ∫_{Ioi 0} g(y) dy.

Русский

При p > 0 та же формула замены переменной без модуля в множителе Якоби сохраняется: ∫ p x^{p-1} g(x^p) dx = ∫ g(y) dy.

LaTeX

$$$$ \int_{x \in Ioi 0} (p \; x^{p-1}) \; g(x^p) \, dx = \int_{y \in Ioi 0} g(y) \, dy, \quad p > 0. $$$$

Lean4

theorem integral_comp_rpow_Ioi_of_pos {g : ℝ → E} {p : ℝ} (hp : 0 < p) :
    (∫ x in Ioi 0, (p * x ^ (p - 1)) • g (x ^ p)) = ∫ y in Ioi 0, g y :=
  by
  convert integral_comp_rpow_Ioi g hp.ne'
  rw [abs_of_nonneg hp.le]

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