no goals
α : Type u_2
β : Type u_1
γ : Type ?u.66368
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
⊢ ↑(toOuterMeasure (bind p f)) s = ∑' (b : β), if b ∈ s then ∑' (a : α), ↑p a * ↑(f a) b else 0
simp [toOuterMeasure_apply, Set.indicator_apply]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.66368
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
b : β
⊢ (if b ∈ s then ∑' (a : α), ↑p a * ↑(f a) b else 0) = ∑' (a : α), ↑p a * if b ∈ s then ↑(f a) b else 0
split_ifs <;> simp
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.66368
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
a : α
b : β
⊢ (if b ∈ s then ↑(f a) b else 0) = if b ∈ s then ↑(f a) b else 0
split_ifs <;> rfl
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.66368
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
a : α
⊢ (↑p a * ∑' (b : β), if b ∈ s then ↑(f a) b else 0) = ↑p a * ↑(toOuterMeasure (f a)) s
simp only [toOuterMeasure_apply, Set.indicator_apply]