English
For a function g: ℝ → E and a nonzero exponent p, the substitution y = x^p on the positive half-line Ioi 0 preserves integrability and equality of the integrals with the |p| factor appearing as a Jacobian term.
Русский
Для функции g и ненулевого p замена y = x^p на Ioi 0 сохраняет интегрируемость и равенство интегралов, где появляется множитель |p| как якобиан.
LaTeX
$$$$ \int_{x \in Ioi 0} (|p| \; x^{p-1}) \; g(x^p) \, dx = \int_{y \in Ioi 0} g(y) \, dy, \quad p \neq 0. $$$$
Lean4
/-- Substitution `y = x ^ p` in integrals over `Ioi 0` -/
theorem integral_comp_rpow_Ioi (g : ℝ → E) {p : ℝ} (hp : p ≠ 0) :
(∫ x in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p)) = ∫ y in Ioi 0, g y :=
by
let S := Ioi (0 : ℝ)
have a1 : ∀ x : ℝ, x ∈ S → HasDerivWithinAt (fun t : ℝ => t ^ p) (p * x ^ (p - 1)) S x := fun x hx =>
(hasDerivAt_rpow_const (Or.inl (mem_Ioi.mp hx).ne')).hasDerivWithinAt
have a2 : InjOn (fun x : ℝ => x ^ p) S :=
by
rcases lt_or_gt_of_ne hp with (h | h)
· apply StrictAntiOn.injOn
intro x hx y hy hxy
rw [← inv_lt_inv₀ (rpow_pos_of_pos hx p) (rpow_pos_of_pos hy p), ← rpow_neg (le_of_lt hx), ←
rpow_neg (le_of_lt hy)]
exact rpow_lt_rpow (le_of_lt hx) hxy (neg_pos.mpr h)
exact StrictMonoOn.injOn fun x hx y _ hxy => rpow_lt_rpow (mem_Ioi.mp hx).le hxy h
have a3 : (fun t : ℝ => t ^ p) '' S = S := by
ext1 x; rw [mem_image]; constructor
· rintro ⟨y, hy, rfl⟩; exact rpow_pos_of_pos hy p
· intro hx; refine ⟨x ^ (1 / p), rpow_pos_of_pos hx _, ?_⟩
rw [← rpow_mul (le_of_lt hx), one_div_mul_cancel hp, rpow_one]
have := integral_image_eq_integral_abs_deriv_smul measurableSet_Ioi a1 a2 g
rw [a3] at this; rw [this]
refine setIntegral_congr_fun measurableSet_Ioi ?_
intro x hx; dsimp only
rw [abs_mul, abs_of_nonneg (rpow_nonneg (le_of_lt hx) _)]
