expect_congr — Mathlib

English

If s=t and f(i)=g(i) for all i∈t, then their expectations are equal: 𝔼 i∈s f i = 𝔼 i∈t g i.

Русский

Если s=t и f(i)=g(i) для всех i∈t, то их ожидания равны.

LaTeX

$$$$ \\text{If } s=t \\text{ and } \\forall i \\in t,\\ f(i)=g(i), \\quad \\mathbb{E}_{i \\in s} f(i) = \\mathbb{E}_{i \\in t} g(i). $$$$

Lean4

@[congr]
theorem expect_congr {t : Finset ι} (hst : s = t) (h : ∀ i ∈ t, f i = g i) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by
  rw [expect, expect, sum_congr hst h, hst]

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