integrableOn_Ioi_comp_rpow_iff' — Mathlib

English

The substitution y = x^p on Ioi 0 preserves integrability without the |p| factor, i.e., IntegrableOn (x^{p-1} • f(x^p)) on Ioi 0 iff IntegrableOn f on Ioi 0, with hp ≠ 0.

Русский

Замена y = x^p на Ioi 0 сохраняет интегрируемость без модуля |p|, если p ≠ 0.

LaTeX

$$$$ \text{IntegrableOn}(x^{p-1} \cdot f(x^p), Ioi 0) \iff \text{IntegrableOn}(f, Ioi 0). $$$$

Lean4

/-- The substitution `y = x ^ p` in integrals over `Ioi 0` preserves integrability (version
without `|p|` factor) -/
theorem integrableOn_Ioi_comp_rpow_iff' [NormedSpace ℝ E] (f : ℝ → E) {p : ℝ} (hp : p ≠ 0) :
    IntegrableOn (fun x => x ^ (p - 1) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0) := by
  simpa only [← integrableOn_Ioi_comp_rpow_iff f hp, mul_smul] using (integrable_smul_iff (abs_pos.mpr hp).ne' _).symm

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