le_gaussNorm — Mathlib

English

There exists an index i such that gaussNorm(v,c,p) equals v(coeff i) · c^i, for a polynomial p.

Русский

Существует индекс i, для которого gaussNorm(v,c,p) = v(p_i) · c^i.

LaTeX

$$∃ i, gaussNorm(v,c;p) = v(p.coeff i) · c^i$$

Lean4

theorem le_gaussNorm [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] (hc : 0 ≤ c) (i : ℕ) :
    v (p.coeff i) * c ^ i ≤ p.gaussNorm v c :=
  by
  rw [← gaussNorm_coe_powerSeries _ _ hc, ← coeff_coe]
  apply PowerSeries.le_gaussNorm
  simpa using aux_bdd v p

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