Theorems · Theorem · real analysis

integrableOn_add_rpow_Ioi_of_lt

∀ {a c m : ℝ}, a < -1 → -m < c → MeasureTheory.IntegrableOn (fun x => (x + m) ^ a) (Set.Ioi c) MeasureTheory.volume

If -m < c, then (fun t : ℝ ↦ (t + m) ^ a) is integrable on (c, ∞) for all a < -1.

Defined in

Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Cited by

1 results in Mathlib

Foundations

Depth 269 from the axioms · uses propext, Classical.choice, Quot.sound