summable_one_div_rpow

Mathlib.Analysis.PSeries

URI: https://scilib.ai/kg/mathlib#NNReal.summable_one_div_rpow

English

For p real, the series ∑ 1/(n^p) converges iff p > 1, in the NNReal setting.

Русский

Для действительного p ряд ∑ 1/(n^p) сходится и только тогда, когда p > 1, в контексте NNReal.

LaTeX

$$$$\displaystyle \sum_{n=1}^{\infty} \frac{1}{n^{p}} < \infty \quad\text{iff } p>1.$$$$

Lean4

theorem summable_one_div_rpow {p : ℝ} : Summable (fun n => 1 / (n : ℝ≥0) ^ p : ℕ → ℝ≥0) ↔ 1 < p := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru