gaussNorm_nonneg — Mathlib

English

If c ≥ 0 and v is a nonnegative linear functional with respect to real-valued outputs, then gaussNorm(v,c,p) ≥ 0 for any p.

Русский

Если c ≥ 0 и v положительно-однозначная линейная функциональная карта, то gaussNorm(v,c,p) ≥ 0 для любого p.

LaTeX

$$gaussNorm(v,c,p) ≥ 0$$

Lean4

theorem gaussNorm_nonneg (hc : 0 ≤ c) [NonnegHomClass F R ℝ] : 0 ≤ p.gaussNorm v c := by
  by_cases hp : p.support.Nonempty <;> simp_all [gaussNorm, sup'_nonneg_of_ne_zero, -Finset.le_sup'_iff]

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