expect_pos — Mathlib

English

If m is subadditive and respects division and p is preserved, then for any nonempty s with p(f i) for all i, the bound holds.

Русский

Если m субаддитивна и p сохраняется, то для непустого s с p(f i) выполняется граница.

LaTeX

$$$s.Nonempty → (∀ i∈s, p(f(i))) → m(\\mathbb{E}_{i∈s} f(i)) ≤ \\mathbb{E}_{i∈s} m(f(i))$$$

Lean4

theorem expect_pos (hf : ∀ i ∈ s, 0 < f i) (hs : s.Nonempty) : 0 < 𝔼 i ∈ s, f i :=
  smul_pos (inv_pos.2 <| mod_cast hs.card_pos) <| sum_pos hf hs

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