English
For a nonzero p, the substitution y = x^p preserves integrability on Ioi 0 up to an rpow factor: IntegrableOn ((|p|) x^{p-1} • f(x^p)) on Ioi 0 iff IntegrableOn f on Ioi 0.
Русский
При p ≠ 0 подстановка y = x^p сохраняет интегрируемость на Ioi 0 для соответствующей x^{p-1} и f(x^p).
LaTeX
$$$$ \text{IntegrableOn} \ (\, (|p|) \cdot x^{p-1} \cdot f(x^p) \,, \; Ioi\ 0) \; \Leftrightarrow \; \text{IntegrableOn}(f, Ioi 0). $$$$
Lean4
/-- The substitution `y = x ^ p` in integrals over `Ioi 0` preserves integrability. -/
theorem integrableOn_Ioi_comp_rpow_iff [NormedSpace ℝ E] (f : ℝ → E) {p : ℝ} (hp : p ≠ 0) :
IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0) :=
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 _hy 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 := integrableOn_image_iff_integrableOn_abs_deriv_smul measurableSet_Ioi a1 a2 f
rw [a3] at this
rw [this]
refine integrableOn_congr_fun (fun x hx => ?_) measurableSet_Ioi
simp_rw [abs_mul, abs_of_nonneg (rpow_nonneg (le_of_lt hx) _)]
