expect_eq_zero_iff_of_nonpos — Mathlib

English

In a finite index set, if all entries are nonnegative, the average is zero iff all entries are zero; a related variant with nonpositive values holds similarly.

Русский

Для конечного индекса среднее нулевого элемента эквивалентно нулю во всех местах; аналогично для неотрицательных/неположительных значений.

LaTeX

$$$[Nonempty] \\Rightarrow (hf : f \\ge 0) \\Rightarrow (\\mathbb{E}_{i} f_i = 0 \\iff f = 0)$$$

Lean4

theorem expect_eq_zero_iff_of_nonpos [Nonempty ι] (hf : f ≤ 0) : 𝔼 i, f i = 0 ↔ f = 0 := by
  simp [expect, sum_eq_zero_iff_of_nonpos hf]

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