gaussNorm_nonneg — Mathlib

English

If v maps to nonnegative reals (NonnegHomClass), then gaussNorm(v,c,f) ≥ 0 for any f.

Русский

Если v принимает значения в неотрицательных вещественных числах (NonnegHomClass), то gaussNorm(v,c,f) неотрицательно.

LaTeX

$$$ 0 \leq \mathrm{gaussNorm}(v,c,f) $$$

Lean4

theorem gaussNorm_nonneg [NonnegHomClass F R ℝ] : 0 ≤ f.gaussNorm v c :=
  by
  by_cases h : BddAbove (Set.range fun i ↦ v (f.coeff i) * c ^ i)
  ·
    calc
      0 ≤ v (f.coeff 0) * c ^ 0 := mul_nonneg (apply_nonneg v (f.coeff 0)) <| pow_nonneg (le_of_lt (zero_lt_one)) 0
      _ ≤ f.gaussNorm v c := le_ciSup h 0
  · simp [gaussNorm, h]

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