intervalIntegrable_rpow — Mathlib

English

For r ∈ ℝ, if 0 ≤ r or 0 ∉ [a, b], then x ↦ x^r is interval-integrable on [a, b] with respect to μ.

Русский

Для r ∈ ℝ, если 0 ≤ r или 0 ∉ [a, b], то x^r интегрируема по интервалу [a, b] относительно μ.

LaTeX

$$$\\\\forall a,b \\\\in \\\\mathbb{R}, \\\\[ \\\\mu \\\] \\\\text{IntervalIntegrable}(x \\\\mapsto x^{r}) \\\\ a \\\\ b,$ где $r \ge 0$ или $0 \notin [a,b].$$$

Lean4

/-- See `intervalIntegrable_rpow'` for a version with a weaker hypothesis on `r`, but assuming the
measure is volume. -/
theorem intervalIntegrable_rpow {r : ℝ} (h : 0 ≤ r ∨ (0 : ℝ) ∉ [[a, b]]) : IntervalIntegrable (fun x => x ^ r) μ a b :=
  (continuousOn_id.rpow_const fun _ hx => h.symm.imp (ne_of_mem_of_not_mem hx) id).intervalIntegrable

Похожие утверждения