gaussNorm — Mathlib

English

The Gauss norm gaussNorm of a power series f with v and c is defined as the supremum over natural numbers i of v(f.coeff i) · c^i.

Русский

Гауссова норма gaussNorm степенного ряда f по отображению v и константе c равна наибольшей верхней границе чисел v(f_i) · c^i по всем i ∈ ℕ.

LaTeX

$$$ \mathrm{gaussNorm}(v,c,f) = \sup_{i \in \mathbb{N}} \, v(f_{i}) \cdot c^{i} $$$

Lean4

/-- Given a power series `f` in `R⟦X⟧`, a function `v : R → ℝ` and a real number `c`, the Gauss norm
is defined as the supremum of the set of all values of `v (f.coeff i) * c ^ i` for all `i : ℕ`. -/
noncomputable def gaussNorm : ℝ :=
  ⨆ i : ℕ, v (f.coeff i) * c ^ i

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