smoothingSeminormSeq — Mathlib

English

For a ring seminorm μ on a commutative ring R, and x ∈ R, the real-valued sequence defined by a_n = μ(x^n)^{1/n} is considered: smoothingSeminormSeq(x) = (n ↦ μ(x^n)^{1/n}).

Русский

Для кольцевой семиномормы μ на R и элемента x ∈ R последовательность a_n = μ(x^n)^{1/n} задаётся как smoothingSeminormSeq(x).

LaTeX

$$$\text{ smoothingSeminormSeq }(x) : \mathbb{N} \to \mathbb{R},\quad n \mapsto \mu(x^n)^{1/n}$$$

Lean4

/-- The `ℝ`-valued sequence sending `n` to `(μ (x ^ n))^(1/n : ℝ)`. -/
abbrev smoothingSeminormSeq (x : R) : ℕ → ℝ := fun n => μ (x ^ n) ^ (1 / n : ℝ)

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