le_changeOriginSeries_radius — Mathlib

English

For each k, the radius of p.changeOriginSeries is at least as large as the original radius, giving a lower bound on radii under origin change.

Русский

Для каждого k радиус p.changeOriginSeries не меньше исходного радиуса, то есть при переносе начала радиус не уменьшается.

LaTeX

$$$p.radius \\le (p.changeOriginSeries k).radius$$$

Lean4

theorem le_changeOriginSeries_radius (k : ℕ) : p.radius ≤ (p.changeOriginSeries k).radius :=
  ENNReal.le_of_forall_nnreal_lt fun _r hr => le_radius_of_summable_nnnorm _ (p.changeOriginSeries_summable_aux₃ hr k)

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