English
The Gauss norm of a polynomial p ∈ R[X], with a function v : R → ℝ and a real c, is defined as the supremum of the values v(coeff i) · c^i over all indices i in the support of p; if the support is empty, the norm is 0.
Русский
Гауссова норма многочлена p ∈ R[X] с функцией v: R → ℝ и вещественным c определяется как наибольшая верхняя граница значений v(coeff i)·c^i по всем i в поддержке p; если поддержка пуста, норма равна 0.
LaTeX
$$$\\operatorname{gaussNorm}(v,c;p)=\\begin{cases} \\operatorname{sup}_{i\\in\\mathrm{supp}(p)} \\, v(p_i) \\cdot c^i, & \\mathrm{supp}(p) \\neq \\varnothing, \\\\ 0, & \\mathrm{supp}(p)=\\varnothing.\\end{cases}$$$
Lean4
/-- Given a polynomial `p` 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 (p.coeff i) * c ^ i` for all `i` in the
support of `p`. -/
def gaussNorm : ℝ :=
if h : p.support.Nonempty then p.support.sup' h fun i ↦ (v (p.coeff i) * c ^ i) else 0
