formalMultilinearSeries_geometric_apply_norm

English

For each n, the norm of the nth geometric coefficient is bounded by max{1, ||1||}. Moreover, the radius is at least 1.

Русский

Для каждого n норма n-й компонент геометрического коэффициента ограничена максимумом {1, ||1||}. Радиус не менее 1.

LaTeX

$$$\forall n, \|\mathrm{formalMultilinearSeries_geometric }\mathbb{K} A\, n\| \le \max\{1, \|1\|\}, \text{ and } 1 \le (\mathrm{radius}(\mathrm{formalMultilinearSeries_geometric }\mathbb{K} A))$$$

Lean4

theorem formalMultilinearSeries_geometric_apply_norm [NormOneClass A] (n : ℕ) :
    ‖formalMultilinearSeries_geometric 𝕜 A n‖ = 1 :=
  ContinuousMultilinearMap.norm_mkPiAlgebraFin

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