Theorems · Theorem · real analysis

intervalIntegral.intervalIntegrable_rpow

∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {r : ℝ},
  0 ≤ r ∨ 0 ∉ Set.uIcc a b → IntervalIntegrable (fun x => x ^ r) μ a b

See intervalIntegrable_rpow' for a version with a weaker hypothesis on r, but assuming the measure is volume.

Defined in

Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsLocallyFiniteMeasure