English
The function x ↦ x^−1 is interval integrable on [a,b] if and only if a = b or 0 ∉ [a,b].
Русский
Функция x ↦ x^−1 интегрируема по интервалу [a,b] тогда и только тогда, когда a = b или 0 ∉ [a,b].
LaTeX
$$$\\text{IntervalIntegrable}(x \\mapsto x^{-1}, \\text{volume}, a, b) \\iff a = b \\lor 0 \\notin [[a,b]]$$$
Lean4
/-- The function `fun x => (x - c)⁻¹` is integrable on `a..b` if and only if
`a = b` or `c ∉ [a, b]`. -/
@[simp]
theorem intervalIntegrable_sub_inv_iff {a b c : ℝ} :
IntervalIntegrable (fun x => (x - c)⁻¹) volume a b ↔ a = b ∨ c ∉ [[a, b]] :=
by
constructor
· refine fun h => or_iff_not_imp_left.2 fun hne hc => ?_
exact not_intervalIntegrable_of_sub_inv_isBigO_punctured (isBigO_refl _ _) hne hc h
· rintro (rfl | h₀)
· exact IntervalIntegrable.refl
refine ((continuous_sub_right c).continuousOn.inv₀ ?_).intervalIntegrable
exact fun x hx => sub_ne_zero.2 <| ne_of_mem_of_not_mem hx h₀
