case refine'_1
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
p : Pmf α
s t : Set α
h : (∑' (x : α), Set.indicator s (↑p) x) = 1
a : α
hap : a ∈ support p
⊢ a ∈ s

case refine'_2
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
p : Pmf α
s t : Set α
h : support p ⊆ s
⊢ (∑' (x : α), Set.indicator s (↑p) x) = 1
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
p : Pmf α
s t : Set α
⊢ ↑(toOuterMeasure p) s = 1 ↔ support p ⊆ s
refine' (p.toOuterMeasure_apply s).symm ▸ ⟨fun h a hap => _, fun h => _⟩
case refine'_1
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
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
case refine'_1
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
p : Pmf α
s t : Set α
h : (∑' (x : α), Set.indicator s (↑p) x) = 1
a : α
hap : a ∈ support p
⊢ a ∈ s
refine' by_contra fun hs => ne_of_lt _ (h.trans p.tsum_coe.symm)
case refine'_1
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
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
case refine'_1
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
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
have hs' : s.indicator p a = 0 := Set.indicator_apply_eq_zero.2 fun hs' => False.elim <| hs hs'
case refine'_1
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
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
case refine'_1
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
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
have hsa : s.indicator p a < p a := hs'.symm ▸ (p.apply_pos_iff a).2 hap
no goals
case refine'_1
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
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
exact ENNReal.tsum_lt_tsum (p.tsum_coe_indicator_ne_top s)
  (fun x => Set.indicator_apply_le fun _ => le_rfl) hsa
case refine'_2
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
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.26301
γ : Type ?u.26304
p : Pmf α
s t : Set α
h : support p ⊆ s
⊢ ∀ (x : α), ¬x ∈ s → ↑p x = 0
case refine'_2
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
p : Pmf α
s t : Set α
h : support p ⊆ s
⊢ (∑' (x : α), Set.indicator s (↑p) x) = 1
suffices : ∀ (x) (_ : x ∉ s), p x = 0
case this
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
p : Pmf α
s t : Set α
h : support p ⊆ s
⊢ ∀ (x : α), ¬x ∈ s → ↑p x = 0
case refine'_2
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
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.26301
γ : Type ?u.26304
p : Pmf α
s t : Set α
h : support p ⊆ s
⊢ ∀ (x : α), ¬x ∈ s → ↑p x = 0
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
no goals
case this
α : Type u_1
β : Type ?u.26301
γ : Type ?u.26304
p : Pmf α
s t : Set α
h : support p ⊆ s
⊢ ∀ (x : α), ¬x ∈ s → ↑p x = 0
exact fun a ha => (p.apply_eq_zero_iff a).2 <| Set.not_mem_subset h ha