intervalIntegrable_zpow — Mathlib

English

For a, b ∈ ℝ, μ locally finite, and integer n ∈ ℤ, the function x ↦ x^n is interval-integrable on [a, b] provided either n ≥ 0 or 0 ∉ [a, b].

Русский

Для a, b ∈ ℝ, μ локально конечна и целочисленный показатель n ∈ ℤ, функция x^n интегрируема по интервалу на [a, b], если либо n ≥ 0, либо 0 не принадлежит [a, b].

LaTeX

$$$\\\\forall a,b \\\\in \\\\mathbb{R}, \\\\[ \\\\mu \\\] \\\\text{IntervalIntegrable}(x \\\\mapsto x^{n}) \\\\ a \\\\ b \\\\text{, если } (0 \\\\le n) \\\\lor \\\\ (0 \\\\in [a,b]^{c}).$$$

Lean4

theorem intervalIntegrable_zpow {n : ℤ} (h : 0 ≤ n ∨ (0 : ℝ) ∉ [[a, b]]) : IntervalIntegrable (fun x => x ^ n) μ a b :=
  (continuousOn_id.zpow₀ n fun _ hx => h.symm.imp (ne_of_mem_of_not_mem hx) id).intervalIntegrable

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