Integrability of Special Functions

This file establishes basic facts about the interval integrability of special functions, including powers and the logarithm.

@[simp]

theorem intervalIntegral.intervalIntegrable_pow {a b : ℝ} (n : ℕ) {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable (fun (x : ℝ) => x ^ n) μ a b

theorem intervalIntegral.intervalIntegrable_zpow {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {n : ℤ} (h : 0 ≤ n ∨ 0 ∉ Set.uIcc a b) : IntervalIntegrable (fun (x : ℝ) => x ^ n) μ a b

theorem intervalIntegral.intervalIntegrable_rpow {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {r : ℝ} (h : 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.

theorem intervalIntegral.intervalIntegrable_rpow' {a b r : ℝ} (h : -1 < r) : IntervalIntegrable (fun (x : ℝ) => x ^ r) MeasureTheory.volume a b

See intervalIntegrable_rpow for a version applying to any locally finite measure, but with a stronger hypothesis on r.

theorem intervalIntegral.integrableOn_Ioo_rpow_iff {s t : ℝ} (ht : 0 < t) : MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ s) (Set.Ioo 0 t) MeasureTheory.volume ↔ -1 < s

The power function x ↦ x^s is integrable on (0, t) iff -1 < s.

theorem intervalIntegral.intervalIntegrable_cpow {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {r : ℂ} (h : 0 ≤ r.re ∨ 0 ∉ Set.uIcc a b) : IntervalIntegrable (fun (x : ℝ) => ↑x ^ r) μ a b

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

theorem intervalIntegral.intervalIntegrable_cpow' {a b : ℝ} {r : ℂ} (h : -1 < r.re) : IntervalIntegrable (fun (x : ℝ) => ↑x ^ r) MeasureTheory.volume a b

See intervalIntegrable_cpow for a version applying to any locally finite measure, but with a stronger hypothesis on r.

theorem intervalIntegral.integrableOn_Ioo_cpow_iff {s : ℂ} {t : ℝ} (ht : 0 < t) : MeasureTheory.IntegrableOn (fun (x : ℝ) => ↑x ^ s) (Set.Ioo 0 t) MeasureTheory.volume ↔ -1 < s.re

The complex power function x ↦ x^s is integrable on (0, t) iff -1 < s.re.

@[simp]

theorem intervalIntegral.intervalIntegrable_id {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable (fun (x : ℝ) => x) μ a b

theorem intervalIntegral.intervalIntegrable_const {a b c : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable (fun (x : ℝ) => c) μ a b

theorem intervalIntegral.intervalIntegrable_one_div {a b : ℝ} {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] (h : ∀ x ∈ Set.uIcc a b, f x ≠ 0) (hf : ContinuousOn f (Set.uIcc a b)) : IntervalIntegrable (fun (x : ℝ) => 1 / f x) μ a b

@[simp]

theorem intervalIntegral.intervalIntegrable_inv {a b : ℝ} {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] (h : ∀ x ∈ Set.uIcc a b, f x ≠ 0) (hf : ContinuousOn f (Set.uIcc a b)) : IntervalIntegrable (fun (x : ℝ) => (f x)⁻¹) μ a b

@[simp]

theorem intervalIntegral.intervalIntegrable_sin {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable Real.sin μ a b

@[simp]

theorem intervalIntegral.intervalIntegrable_cos {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable Real.cos μ a b

@[simp]

theorem intervalIntegral.intervalIntegrable_exp {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable Real.exp μ a b

@[simp]

theorem IntervalIntegrable.log {a b : ℝ} {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] (hf : ContinuousOn f (Set.uIcc a b)) (h : ∀ x ∈ Set.uIcc a b, f x ≠ 0) : IntervalIntegrable (fun (x : ℝ) => Real.log (f x)) μ a b

@[simp]

theorem intervalIntegral.intervalIntegrable_log {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] (h : 0 ∉ Set.uIcc a b) : IntervalIntegrable Real.log μ a b

The real logarithm is interval integrable (with respect to every locally finite measure) over every interval that does not contain zero. See intervalIntegrable_log' for a version without any hypothesis on the interval, but assuming the measure is the volume.

@[simp]

theorem intervalIntegral.intervalIntegrable_log' {a b : ℝ} : IntervalIntegrable Real.log MeasureTheory.volume a b

The real logarithm is interval integrable (with respect to the volume measure) on every interval. See intervalIntegrable_log for a version applying to any locally finite measure, but with an additional hypothesis on the interval.

theorem intervalIntegral.intervalIntegrable_one_div_one_add_sq {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable (fun (x : ℝ) => 1 / (1 + x ^ 2)) μ a b

@[simp]

theorem intervalIntegral.intervalIntegrable_inv_one_add_sq {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable (fun (x : ℝ) => (1 + x ^ 2)⁻¹) μ a b