α : Type u_2
β : Type u_1
γ : Type ?u.144355
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
⊢ (∑' (x : β), if x ∈ s then ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0)) x else 0) =
    ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ∑' (x : β), if x ∈ s then ↑(f a (_ : ¬↑p a = 0)) x else 0
α : Type u_2
β : Type u_1
γ : Type ?u.144355
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
⊢ ↑(toOuterMeasure (bindOnSupport p f)) s = ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(toOuterMeasure (f a h)) s
simp only [toOuterMeasure_apply, Set.indicator_apply, bindOnSupport_apply]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.144355
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
⊢ (∑' (x : β), if x ∈ s then ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0)) x else 0) =
    ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ∑' (x : β), if x ∈ s then ↑(f a (_ : ¬↑p a = 0)) x else 0
calc
  (∑' b, ite (b ∈ s) (∑' a, p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0) =
      ∑' (b) (a), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
    tsum_congr fun b => by split_ifs with hbs <;> simp only [eq_self_iff_true, tsum_zero]
  _ = ∑' (a) (b), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
    ENNReal.tsum_comm
  _ = ∑' a, p a * ∑' b, ite (b ∈ s) (dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
    (tsum_congr fun a => by simp only [← ENNReal.tsum_mul_left, mul_ite, MulZeroClass.mul_zero])
  _ = ∑' a, p a * dite (p a = 0) (fun h => 0) fun h => ∑' b, ite (b ∈ s) (f a h b) 0 :=
    tsum_congr fun a => by split_ifs with ha <;> simp only [ite_self, tsum_zero, eq_self_iff_true]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.144355
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
b : β
⊢ (if b ∈ s then ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b else 0) =
    ∑' (a : α), if b ∈ s then ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b else 0
split_ifs with hbs <;> simp only [eq_self_iff_true, tsum_zero]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.144355
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
a : α
⊢ (∑' (b : β), if b ∈ s then ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b else 0) =
    ↑p a * ∑' (b : β), if b ∈ s then if h : ↑p a = 0 then 0 else ↑(f a h) b else 0
simp only [← ENNReal.tsum_mul_left, mul_ite, MulZeroClass.mul_zero]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.144355
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
a : α
⊢ (↑p a * ∑' (b : β), if b ∈ s then if h : ↑p a = 0 then 0 else ↑(f a h) b else 0) =
    ↑p a * if h : ↑p a = 0 then 0 else ∑' (b : β), if b ∈ s then ↑(f a h) b else 0
split_ifs with ha <;> simp only [ite_self, tsum_zero, eq_self_iff_true]