[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
⊢ ↑p a = 0 ↔ ¬a ∈ support p
[PROOFSTEP]
rw [mem_support_iff, Classical.not_not]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
⊢ ↑p a = 1 ↔ support p = {a}
[PROOFSTEP]
refine'
  ⟨fun h =>
    Set.Subset.antisymm (fun a' ha' => by_contra fun ha => _) fun a' ha' =>
      ha'.symm ▸ (p.mem_support_iff a).2 fun ha => zero_ne_one <| ha.symm.trans h,
    fun h => _root_.trans (symm <| tsum_eq_single a fun a' ha' => (p.apply_eq_zero_iff a').2 (h.symm ▸ ha')) p.tsum_coe⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
⊢ False
[PROOFSTEP]
suffices : 1 < ∑' a, p a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 1 < ∑' (a : α), ↑p a
⊢ False
case this
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
⊢ 1 < ∑' (a : α), ↑p a
[PROOFSTEP]
exact ne_of_lt this p.tsum_coe.symm
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
⊢ 1 < ∑' (a : α), ↑p a
[PROOFSTEP]
have : 0 < ∑' b, ite (b = a) 0 (p b) :=
  lt_of_le_of_ne' zero_le'
    ((tsum_ne_zero_iff ENNReal.summable).2 ⟨a', ite_ne_left_iff.2 ⟨ha, Ne.symm <| (p.mem_support_iff a').2 ha'⟩⟩)
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
⊢ 1 < ∑' (a : α), ↑p a
[PROOFSTEP]
calc
  1 = 1 + 0 := (add_zero 1).symm
  _ < p a + ∑' b, ite (b = a) 0 (p b) := (ENNReal.add_lt_add_of_le_of_lt ENNReal.one_ne_top (le_of_eq h.symm) this)
  _ = ite (a = a) (p a) 0 + ∑' b, ite (b = a) 0 (p b) := by rw [eq_self_iff_true, if_true]
  _ = (∑' b, ite (b = a) (p b) 0) + ∑' b, ite (b = a) 0 (p b) :=
    by
    congr
    exact symm (tsum_eq_single a fun b hb => if_neg hb)
  _ = ∑' b, (ite (b = a) (p b) 0 + ite (b = a) 0 (p b)) := ENNReal.tsum_add.symm
  _ = ∑' b, p b := tsum_congr fun b => by split_ifs <;> simp only [zero_add, add_zero, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
⊢ (↑p a + ∑' (b : α), if b = a then 0 else ↑p b) = (if a = a then ↑p a else 0) + ∑' (b : α), if b = a then 0 else ↑p b
[PROOFSTEP]
rw [eq_self_iff_true, if_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
⊢ ((if a = a then ↑p a else 0) + ∑' (b : α), if b = a then 0 else ↑p b) =
    (∑' (b : α), if b = a then ↑p b else 0) + ∑' (b : α), if b = a then 0 else ↑p b
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
⊢ (if a = a then ↑p a else 0) = ∑' (b : α), if b = a then ↑p b else 0
[PROOFSTEP]
exact symm (tsum_eq_single a fun b hb => if_neg hb)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
b : α
⊢ ((if b = a then ↑p b else 0) + if b = a then 0 else ↑p b) = ↑p b
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
b : α
h✝ : b = a
⊢ ↑p b + 0 = ↑p b
[PROOFSTEP]
simp only [zero_add, add_zero, le_rfl]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
h : ↑p a = 1
a' : α
ha' : a' ∈ support p
ha : ¬a' ∈ {a}
this : 0 < ∑' (b : α), if b = a then 0 else ↑p b
b : α
h✝ : ¬b = a
⊢ 0 + ↑p b = ↑p b
[PROOFSTEP]
simp only [zero_add, add_zero, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a : α
⊢ ↑p a ≤ 1
[PROOFSTEP]
refine' hasSum_le (fun b => _) (hasSum_ite_eq a (p a)) (hasSum_coe_one p)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a b : α
⊢ (if b = a then ↑p a else 0) ≤ ↑p b
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a b : α
h : b = a
⊢ ↑p a ≤ ↑p b
[PROOFSTEP]
simp only [h, zero_le', le_rfl]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
a b : α
h : ¬b = a
⊢ 0 ≤ ↑p b
[PROOFSTEP]
simp only [h, zero_le', le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
⊢ OuterMeasure.caratheodory (toOuterMeasure p) = ⊤
[PROOFSTEP]
refine' eq_top_iff.2 <| le_trans (le_sInf fun x hx => _) (le_sum_caratheodory _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
x : MeasurableSpace α
hx : x ∈ Set.range fun i => OuterMeasure.caratheodory (↑p i • dirac i)
⊢ ⊤ ≤ x
[PROOFSTEP]
have ⟨y, hy⟩ := hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
x : MeasurableSpace α
hx : x ∈ Set.range fun i => OuterMeasure.caratheodory (↑p i • dirac i)
y : α
hy : (fun i => OuterMeasure.caratheodory (↑p i • dirac i)) y = x
⊢ ⊤ ≤ x
[PROOFSTEP]
exact ((le_of_eq (dirac_caratheodory y).symm).trans (le_smul_caratheodory _ _)).trans (le_of_eq hy)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s✝ t : Set α
s : Finset α
⊢ ↑(toOuterMeasure p) ↑s = ∑ x in s, ↑p x
[PROOFSTEP]
refine' (toOuterMeasure_apply p s).trans ((tsum_eq_sum (s := s) _).trans _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s✝ t : Set α
s : Finset α
⊢ ∀ (b : α), ¬b ∈ s → Set.indicator (↑s) (↑p) b = 0
[PROOFSTEP]
exact fun x hx => Set.indicator_of_not_mem (Finset.mem_coe.not.2 hx) _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s✝ t : Set α
s : Finset α
⊢ ∑ b in s, Set.indicator (↑s) (↑p) b = ∑ x in s, ↑p x
[PROOFSTEP]
exact Finset.sum_congr rfl fun x hx => Set.indicator_of_mem (Finset.mem_coe.2 hx) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
a : α
⊢ ↑(toOuterMeasure p) {a} = ↑p a
[PROOFSTEP]
refine' (p.toOuterMeasure_apply { a }).trans ((tsum_eq_single a fun b hb => _).trans _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
a b : α
hb : b ≠ a
⊢ Set.indicator {a} (↑p) b = 0
[PROOFSTEP]
exact ite_eq_right_iff.2 fun hb' => False.elim <| hb hb'
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
a : α
⊢ Set.indicator {a} (↑p) a = ↑p a
[PROOFSTEP]
exact ite_eq_left_iff.2 fun ha' => False.elim <| ha' rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
⊢ ↑(toOuterMeasure p) s = 0 ↔ Disjoint (support p) s
[PROOFSTEP]
rw [toOuterMeasure_apply, ENNReal.tsum_eq_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
⊢ (∀ (i : α), Set.indicator s (↑p) i = 0) ↔ Disjoint (support p) s
[PROOFSTEP]
exact Function.funext_iff.symm.trans Set.indicator_eq_zero'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
⊢ ↑(toOuterMeasure p) s = 1 ↔ support p ⊆ s
[PROOFSTEP]
refine' (p.toOuterMeasure_apply s).symm ▸ ⟨fun h a hap => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
h : ∑' (x : α), Set.indicator s (↑p) x = 1
a : α
hap : a ∈ support p
⊢ a ∈ s
[PROOFSTEP]
refine' by_contra fun hs => ne_of_lt _ (h.trans p.tsum_coe.symm)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
h : ∑' (x : α), Set.indicator s (↑p) x = 1
a : α
hap : a ∈ support p
hs : ¬a ∈ s
⊢ ∑' (x : α), Set.indicator s (↑p) x < ∑' (a : α), ↑p a
[PROOFSTEP]
have hs' : s.indicator p a = 0 := Set.indicator_apply_eq_zero.2 fun hs' => False.elim <| hs hs'
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
h : ∑' (x : α), Set.indicator s (↑p) x = 1
a : α
hap : a ∈ support p
hs : ¬a ∈ s
hs' : Set.indicator s (↑p) a = 0
⊢ ∑' (x : α), Set.indicator s (↑p) x < ∑' (a : α), ↑p a
[PROOFSTEP]
have hsa : s.indicator p a < p a := hs'.symm ▸ (p.apply_pos_iff a).2 hap
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
h : ∑' (x : α), Set.indicator s (↑p) x = 1
a : α
hap : a ∈ support p
hs : ¬a ∈ s
hs' : Set.indicator s (↑p) a = 0
hsa : Set.indicator s (↑p) a < ↑p a
⊢ ∑' (x : α), Set.indicator s (↑p) x < ∑' (a : α), ↑p a
[PROOFSTEP]
exact ENNReal.tsum_lt_tsum (p.tsum_coe_indicator_ne_top s) (fun x => Set.indicator_apply_le fun _ => le_rfl) hsa
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
h : support p ⊆ s
⊢ ∑' (x : α), Set.indicator s (↑p) x = 1
[PROOFSTEP]
suffices : ∀ (x) (_ : x ∉ s), p x = 0
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
h : support p ⊆ s
this : ∀ (x : α), ¬x ∈ s → ↑p x = 0
⊢ ∑' (x : α), Set.indicator s (↑p) x = 1
case this α : Type u_1 β : Type u_2 γ : Type u_3 p : Pmf α s t : Set α h : support p ⊆ s ⊢ ∀ (x : α), ¬x ∈ s → ↑p x = 0
[PROOFSTEP]
exact
  _root_.trans (tsum_congr fun a => (Set.indicator_apply s p a).trans (ite_eq_left_iff.2 <| symm ∘ this a)) p.tsum_coe
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
h : support p ⊆ s
⊢ ∀ (x : α), ¬x ∈ s → ↑p x = 0
[PROOFSTEP]
exact fun a ha => (p.apply_eq_zero_iff a).2 <| Set.not_mem_subset h ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s t : Set α
⊢ ↑(toOuterMeasure p) (s ∩ support p) = ↑(toOuterMeasure p) s
[PROOFSTEP]
simp only [toOuterMeasure_apply, Pmf.support, Set.indicator_inter_support]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
p : Pmf α
s t : Set α
a : α
h : MeasurableSet {a}
⊢ ↑↑(toMeasure p) {a} = ↑p a
[PROOFSTEP]
simp [toMeasure_apply_eq_toOuterMeasure_apply _ _ h, toOuterMeasure_apply_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
p : Pmf α
s t : Set α
hs : MeasurableSet s
⊢ ↑↑(toMeasure p) s = 0 ↔ Disjoint (support p) s
[PROOFSTEP]
rw [toMeasure_apply_eq_toOuterMeasure_apply p s hs, toOuterMeasure_apply_eq_zero_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
p : Pmf α
s t : Set α
hs : MeasurableSet s
hp : MeasurableSet (support p)
⊢ ↑↑(toMeasure p) (s ∩ support p) = ↑↑(toMeasure p) s
[PROOFSTEP]
simp [p.toMeasure_apply_eq_toOuterMeasure_apply s hs, p.toMeasure_apply_eq_toOuterMeasure_apply _ (hs.inter hp)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
p : Pmf α
s✝ t✝ s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : s ∩ support p ⊆ t
⊢ ↑↑(toMeasure p) s ≤ ↑↑(toMeasure p) t
[PROOFSTEP]
simpa only [p.toMeasure_apply_eq_toOuterMeasure_apply, hs, ht] using toOuterMeasure_mono p h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
p : Pmf α
s✝ t✝ s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : s ∩ support p = t ∩ support p
⊢ ↑↑(toMeasure p) s = ↑↑(toMeasure p) t
[PROOFSTEP]
simpa only [p.toMeasure_apply_eq_toOuterMeasure_apply, hs, ht] using toOuterMeasure_apply_eq_of_inter_support_eq p h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : MeasurableSpace α
p : Pmf α
s t : Set α
inst✝ : MeasurableSingletonClass α
⊢ Function.Injective toMeasure
[PROOFSTEP]
intro p q h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : MeasurableSpace α
p✝ : Pmf α
s t : Set α
inst✝ : MeasurableSingletonClass α
p q : Pmf α
h : toMeasure p = toMeasure q
⊢ p = q
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : MeasurableSpace α
p✝ : Pmf α
s t : Set α
inst✝ : MeasurableSingletonClass α
p q : Pmf α
h : toMeasure p = toMeasure q
x : α
⊢ ↑p x = ↑q x
[PROOFSTEP]
rw [← p.toMeasure_apply_singleton x <| measurableSet_singleton x, ←
  q.toMeasure_apply_singleton x <| measurableSet_singleton x, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑(toMeasure (toPmf μ)) s = ↑↑μ s
[PROOFSTEP]
rw [μ.toPmf.toMeasure_apply s hs, ← μ.tsum_indicator_apply_singleton s hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), Set.indicator s (↑(toPmf μ)) x = ∑' (x : α), Set.indicator s (fun x => ↑↑μ {x}) x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
p : Pmf α
⊢ ↑↑(toMeasure p) Set.univ = 1
[PROOFSTEP]
simpa only [MeasurableSet.univ, toMeasure_apply_eq_toOuterMeasure_apply, Set.indicator_univ, toOuterMeasure_apply,
  ENNReal.coe_eq_one] using tsum_coe p
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
p : Pmf α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
x : α
⊢ ↑(Measure.toPmf (toMeasure p)) x = ↑p x
[PROOFSTEP]
rw [← p.toMeasure_apply_singleton x (measurableSet_singleton x), p.toMeasure.toPmf_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : Countable α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
p : Pmf α
μ✝ : Measure α
inst✝¹ : IsProbabilityMeasure μ✝
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ toMeasure p = μ ↔ p = Measure.toPmf μ
[PROOFSTEP]
rw [← toMeasure_inj, Measure.toPmf_toMeasure]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : Countable α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
p : Pmf α
μ✝ : Measure α
inst✝¹ : IsProbabilityMeasure μ✝
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ Measure.toPmf μ = p ↔ μ = toMeasure p
[PROOFSTEP]
rw [← toMeasure_inj, Measure.toPmf_toMeasure]
