English
The outer measure of the bound PMF equals the weighted sum of the outer measures of the conditional PMFs, i.e., (p.bind f).toOuterMeasure(s) = ∑' a p(a) (f(a)).toOuterMeasure(s).
Русский
Внешняя мера связанного распределения равна взвешенной сумме внешних мер условных распределений: (p.bind f).toOuterMeasure(s) = ∑' a p(a) (f(a)).toOuterMeasure(s).
LaTeX
$$$$ (\\mathrm{bind}(p, f)).\\mathrm{toOuterMeasure}(s) = \\sum_{a} p(a) \\cdot (f(a)).toOuterMeasure(s) $$$$
Lean4
@[simp]
theorem toOuterMeasure_bind_apply : (p.bind f).toOuterMeasure s = ∑' a, p a * (f a).toOuterMeasure s := by
classical
calc
(p.bind f).toOuterMeasure s = ∑' b, if b ∈ s then ∑' a, p a * f a b else 0 := by
simp [toOuterMeasure_apply, Set.indicator_apply]
_ = ∑' (b) (a), p a * if b ∈ s then f a b else 0 := (tsum_congr fun b => by split_ifs <;> simp)
_ = ∑' (a) (b), p a * if b ∈ s then f a b else 0 := ENNReal.tsum_comm
_ = ∑' a, p a * ∑' b, if b ∈ s then f a b else 0 := (tsum_congr fun _ => ENNReal.tsum_mul_left)
_ = ∑' a, p a * ∑' b, if b ∈ s then f a b else 0 :=
(tsum_congr fun a => (congr_arg fun x => p a * x) <| tsum_congr fun b => by split_ifs <;> rfl)
_ = ∑' a, p a * (f a).toOuterMeasure s :=
tsum_congr fun a => by simp only [toOuterMeasure_apply, Set.indicator_apply]
