[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b : β
⊢ ↑(map f p) b = ∑' (a : α), if b = f a then ↑p a else 0
[PROOFSTEP]
simp [map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b✝ b : β
⊢ b ∈ support (map f p) ↔ b ∈ f '' support p
[PROOFSTEP]
simp [map, @eq_comm β b]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b : β
⊢ b ∈ support (map f p) ↔ ∃ a, a ∈ support p ∧ f a = b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b : β
g : β → γ
⊢ map g (map f p) = map (g ∘ f) p
[PROOFSTEP]
simp [map, Function.comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b : β
⊢ map (Function.const α b) p = pure b
[PROOFSTEP]
simp only [map, Function.comp, bind_const, Function.const]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b : β
s : Set β
⊢ ↑(toOuterMeasure (map f p)) s = ↑(toOuterMeasure p) (f ⁻¹' s)
[PROOFSTEP]
simp [map, Set.indicator, toOuterMeasure_apply p (f ⁻¹' s)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b : β
s : Set β
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ ↑↑(toMeasure (map f p)) s = ↑↑(toMeasure p) (f ⁻¹' s)
[PROOFSTEP]
rw [toMeasure_apply_eq_toOuterMeasure_apply _ s hs,
  toMeasure_apply_eq_toOuterMeasure_apply _ (f ⁻¹' s) (measurableSet_preimage hf hs)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b : β
s : Set β
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ ↑(toOuterMeasure (map f p)) s = ↑(toOuterMeasure p) (f ⁻¹' s)
[PROOFSTEP]
exact toOuterMeasure_map_apply f p s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
q : Pmf (α → β)
p : Pmf α
b : β
⊢ ↑(seq q p) b = ∑' (f : α → β) (a : α), if b = f a then ↑q f * ↑p a else 0
[PROOFSTEP]
simp only [seq, mul_boole, bind_apply, pure_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
q : Pmf (α → β)
p : Pmf α
b : β
⊢ (∑' (a : α → β), ↑q a * ∑' (a_1 : α), if b = a a_1 then ↑p a_1 else 0) =
    ∑' (f : α → β) (a : α), if b = f a then ↑q f * ↑p a else 0
[PROOFSTEP]
refine' tsum_congr fun f => ENNReal.tsum_mul_left.symm.trans (tsum_congr fun a => _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
q : Pmf (α → β)
p : Pmf α
b : β
f : α → β
a : α
⊢ (↑q f * if b = f a then ↑p a else 0) = if b = f a then ↑q f * ↑p a else 0
[PROOFSTEP]
simpa only [mul_zero] using mul_ite (b = f a) (q f) (p a) 0
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
q : Pmf (α → β)
p : Pmf α
b✝ b : β
⊢ b ∈ support (seq q p) ↔ b ∈ ⋃ (f : α → β) (_ : f ∈ support q), f '' support p
[PROOFSTEP]
simp [-mem_support_iff, seq, @eq_comm β b]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
q : Pmf (α → β)
p : Pmf α
b : β
⊢ b ∈ support (seq q p) ↔ ∃ f, f ∈ support q ∧ b ∈ f '' support p
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → ℝ≥0∞
s : Finset α
h : ∑ a in s, f a = 1
h' : ∀ (a : α), ¬a ∈ s → f a = 0
a : α
⊢ a ∈ support (ofFinset f s h h') ↔ a ∈ ↑s ∩ Function.support f
[PROOFSTEP]
simpa [mem_support_iff] using mt (h' a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → ℝ≥0∞
s : Finset α
h : ∑ a in s, f a = 1
h' : ∀ (a : α), ¬a ∈ s → f a = 0
a : α
⊢ a ∈ support (ofFinset f s h h') ↔ a ∈ s ∧ f a ≠ 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → ℝ≥0∞
hf0 : tsum f ≠ 0
hf : tsum f ≠ ⊤
a : α
⊢ a ∈ support (normalize f hf0 hf) ↔ a ∈ Function.support f
[PROOFSTEP]
simp [hf, mem_support_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → ℝ≥0∞
hf0 : tsum f ≠ 0
hf : tsum f ≠ ⊤
a : α
⊢ a ∈ support (normalize f hf0 hf) ↔ f a ≠ 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s : Set α
h : ∃ a, a ∈ s ∧ a ∈ support p
⊢ tsum (Set.indicator s ↑p) ≠ 0
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s : Set α
h : ∃ a, a ∈ s ∧ a ∈ support p
a : α
⊢ ↑(filter p s h) a = Set.indicator s (↑p) a * (∑' (a' : α), Set.indicator s (↑p) a')⁻¹
[PROOFSTEP]
rw [filter, normalize_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s : Set α
h : ∃ a, a ∈ s ∧ a ∈ support p
a : α
ha : ¬a ∈ s
⊢ ↑(filter p s h) a = 0
[PROOFSTEP]
rw [filter_apply, Set.indicator_apply_eq_zero.mpr fun ha' => absurd ha' ha, zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s : Set α
h : ∃ a, a ∈ s ∧ a ∈ support p
a : α
⊢ ↑(filter p s h) a = 0 ↔ ¬a ∈ s ∨ ¬a ∈ support p
[PROOFSTEP]
erw [apply_eq_zero_iff, support_filter, Set.mem_inter_iff, not_and_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s : Set α
h : ∃ a, a ∈ s ∧ a ∈ support p
a : α
⊢ ↑(filter p s h) a ≠ 0 ↔ a ∈ s ∧ a ∈ support p
[PROOFSTEP]
rw [Ne.def, filter_apply_eq_zero_iff, not_or, Classical.not_not, Classical.not_not]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0∞
h : p ≤ 1
⊢ ∑ a : Bool, (fun b => bif b then p else 1 - p) a = 1
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ support (bernoulli p h) = {b | bif b then p ≠ 0 else p ≠ 1}
[PROOFSTEP]
refine' Set.ext fun b => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0∞
h : p ≤ 1
b✝ b : Bool
⊢ b ∈ support (bernoulli p h) ↔ b ∈ {b | bif b then p ≠ 0 else p ≠ 1}
[PROOFSTEP]
induction b
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ false ∈ support (bernoulli p h) ↔ false ∈ {b | bif b then p ≠ 0 else p ≠ 1}
[PROOFSTEP]
simp_rw [mem_support_iff, bernoulli_apply, Bool.cond_false, Ne.def, tsub_eq_zero_iff_le, not_le]
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ p < 1 ↔ false ∈ {b | bif b then ¬p = 0 else ¬p = 1}
[PROOFSTEP]
exact ⟨ne_of_lt, lt_of_le_of_ne h⟩
[GOAL]
case true
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ true ∈ support (bernoulli p h) ↔ true ∈ {b | bif b then p ≠ 0 else p ≠ 1}
[PROOFSTEP]
simp only [mem_support_iff, bernoulli_apply, Bool.cond_true, Set.mem_setOf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ b ∈ support (bernoulli p h) ↔ bif b then p ≠ 0 else p ≠ 1
[PROOFSTEP]
simp
