intervalIntegrable_pow — Mathlib

English

Let a, b ∈ ℝ, n ∈ ℕ, and μ be a locally finite measure on ℝ. Then the function x ↦ x^n is interval-integrable on [a, b] with respect to μ.

Русский

Пусть a, b ∈ ℝ, n ∈ ℕ, и μ — локально конечная мера на ℝ. Тогда функция x^n интегрируема по интервалу на [a, b] по мере μ.

LaTeX

$$$\\\\forall a,b \\\\in \\\\mathbb{R}, \\\\forall n \\\\in \\\\mathbb{N}, \\\\[ \\\\mu \\\] \\\\text{IntervalIntegrable}(x \\\\mapsto x^{n})\\\\ \\\\mu \\\\ a \\\\ b$$$

Lean4

@[simp]
theorem intervalIntegrable_pow : IntervalIntegrable (fun x => x ^ n) μ a b :=
  (continuous_pow n).intervalIntegrable a b

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