expect_eq_zero_iff_of_nonneg — Mathlib

English

For a nonempty finite index set and nonnegative function on a finite type, the average being zero implies the function is identically zero.

Русский

Для непустого конечного множества индексов и неотрицательной функции на конечном типе среднее равно нулю тогда и только тогда, когда функция тождественно нулевая.

LaTeX

$$$\\text{expect zero iff zero function}$$$

Lean4

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

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