expect_eq_zero_iff_of_nonpos — Mathlib

English

If s is a finite nonempty index set and f(i) ≤ 0 for all i in s, then the expectation over s is ≤ 0; equivalently, the average of nonpositive numbers is nonpositive.

Русский

Пусть индексы образуют конечный ненулевой набор; если все значения f(i) не положительны, то среднее по s не положительно.

LaTeX

$$$s\\neq\\varnothing \\wedge (\\forall i\\in s, f(i) \\le 0) \\Rightarrow s\\!\\!\\text{expect } f \\le 0$$$

Lean4

theorem expect_eq_zero_iff_of_nonpos (hs : s.Nonempty) (hf : ∀ i ∈ s, f i ≤ 0) : 𝔼 i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0 :=
  by simp [expect, sum_eq_zero_iff_of_nonpos hf, hs.ne_empty]

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