Theorems · Theorem · real analysis

intervalIntegrable_sub_inv_iff

∀ {a b c : ℝ}, IntervalIntegrable (fun x => (x - c)⁻¹) MeasureTheory.volume a b ↔ a = b ∨ c ∉ Set.uIcc a b

The function fun x => (x - c)⁻¹ is integrable on a..b if and only if a = b or c ∉ [a, b].

Defined in

Mathlib.Analysis.SpecialFunctions.NonIntegrable

Cited by

0 results in Mathlib

Foundations

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