English
If there is a congruence between predicates on s and t and f agrees with g on t where q holds, the corresponding expectations are equal.
Русский
Если предикаты на s и t совпадают по области определения и f(i)=g(i) на t при выполнении q, то соответствующие ожидания равны.
LaTeX
$$$$ s = t\\; \\Rightarrow\\; (\\forall i \\in t, p(i) \\leftrightarrow q(i)) \\Rightarrow (\\forall i \\in t, q(i) \\Rightarrow f(i)=g(i)) \\Rightarrow \\mathbb{E}_{i \\in s}^{p} f(i) = \\mathbb{E}_{i \\in t}^{q} g(i). $$$$
Lean4
theorem expectWith_congr (hst : s = t) (hpq : ∀ i ∈ t, p i ↔ q i) (h : ∀ i ∈ t, q i → f i = g i) :
𝔼 i ∈ s with p i, f i = 𝔼 i ∈ t with q i, g i :=
expect_congr (by rw [hst, filter_inj'.2 hpq]) <| by simpa using h
