Theorems · Definition · commutative algebra

MvPowerSeries.gaussNorm

{R : Type u_1} → {σ : Type u_2} → (R → ℝ) → (σ → ℝ) → MvPowerSeries σ R → [Semiring R] → ℝ

Given a multivariate power series f in, a function v : R → ℝ and a tuple c of real numbers, the Gauss norm is defined as the supremum of the set of all values of v (coeff t f) * ∏ i : t.support, c i for all t : σ →₀ ℕ.

Defined in

Mathlib.RingTheory.MvPowerSeries.GaussNorm

Cited by

9 results in Mathlib

Foundations

Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Semiring