exists_lt_of_expect_lt — Mathlib

English

If the average over a finite set exceeds a, there exists some index in the set where the corresponding value exceeds a.

Русский

Если среднее по конечному набору больше a, то существует элемент набора с величиной больше a.

LaTeX

$$$s.Nonempty → (\\mathbb{E}_{i∈s} f(i) > a) → ∃ i∈s, f(i) > a$$$

Lean4

theorem exists_lt_of_expect_lt (hs : s.Nonempty) (h : 𝔼 i ∈ s, f i < a) : ∃ x ∈ s, f x < a := by contrapose! h;
  exact le_expect hs h

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