[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
⊢ Pmf α
[PROOFSTEP]
refine' ofFinset (fun a => if a ∈ s then s.card⁻¹ else 0) s _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
⊢ ∑ a in s, (fun a => if a ∈ s then (↑(Finset.card s))⁻¹ else 0) a = 1
[PROOFSTEP]
simp only [Finset.sum_ite_mem, Finset.inter_self, Finset.sum_const, nsmul_eq_mul]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
⊢ ↑(Finset.card s) * (↑(Finset.card s))⁻¹ = 1
[PROOFSTEP]
have : (s.card : ℝ≥0∞) ≠ 0 := by
  simpa only [Ne.def, Nat.cast_eq_zero, Finset.card_eq_zero] using Finset.nonempty_iff_ne_empty.1 hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
⊢ ↑(Finset.card s) ≠ 0
[PROOFSTEP]
simpa only [Ne.def, Nat.cast_eq_zero, Finset.card_eq_zero] using Finset.nonempty_iff_ne_empty.1 hs
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
this : ↑(Finset.card s) ≠ 0
⊢ ↑(Finset.card s) * (↑(Finset.card s))⁻¹ = 1
[PROOFSTEP]
refine' ENNReal.mul_inv_cancel this <| ENNReal.nat_ne_top s.card
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
⊢ ∀ (a : α), ¬a ∈ s → (fun a => if a ∈ s then (↑(Finset.card s))⁻¹ else 0) a = 0
[PROOFSTEP]
exact fun x hx => by simp only [hx, if_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
x : α
hx : ¬x ∈ s
⊢ (fun a => if a ∈ s then (↑(Finset.card s))⁻¹ else 0) x = 0
[PROOFSTEP]
simp only [hx, if_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
ha : a ∈ s
⊢ ↑(uniformOfFinset s hs) a = (↑(Finset.card s))⁻¹
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
ha : ¬a ∈ s
⊢ ↑(uniformOfFinset s hs) a = 0
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
⊢ ∀ (x : α), x ∈ support (uniformOfFinset s hs) ↔ x ∈ ↑s
[PROOFSTEP]
let ⟨a, ha⟩ := hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a✝ a : α
ha : a ∈ s
⊢ ∀ (x : α), x ∈ support (uniformOfFinset s (_ : ∃ x, x ∈ s)) ↔ x ∈ ↑s
[PROOFSTEP]
simp [mem_support_iff, Finset.ne_empty_of_mem ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a✝ a : α
⊢ a ∈ support (uniformOfFinset s hs) ↔ a ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
t : Set α
x : α
⊢ (if x ∈ t then ↑(uniformOfFinset s hs) x else 0) = if x ∈ s ∧ x ∈ t then (↑(Finset.card s))⁻¹ else 0
[PROOFSTEP]
simp_rw [uniformOfFinset_apply, ← ite_and, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
t : Set α
x : α
hx : x ∈ Finset.filter (fun x => x ∈ t) s
⊢ (if x ∈ s ∧ x ∈ t then (↑(Finset.card s))⁻¹ else 0) = (↑(Finset.card s))⁻¹
[PROOFSTEP]
let this : x ∈ s ∧ x ∈ t := by simpa using hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
t : Set α
x : α
hx : x ∈ Finset.filter (fun x => x ∈ t) s
⊢ x ∈ s ∧ x ∈ t
[PROOFSTEP]
simpa using hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
t : Set α
x : α
hx : x ∈ Finset.filter (fun x => x ∈ t) s
this : x ∈ s ∧ x ∈ t := Eq.mp Mathlib.Data.Finset.Basic._auxLemma.130 hx
⊢ (if x ∈ s ∧ x ∈ t then (↑(Finset.card s))⁻¹ else 0) = (↑(Finset.card s))⁻¹
[PROOFSTEP]
simp only [this, and_self_iff, if_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
hs : Finset.Nonempty s
a : α
t : Set α
⊢ ∑ _x in Finset.filter (fun x => x ∈ t) s, (↑(Finset.card s))⁻¹ =
    ↑(Finset.card (Finset.filter (fun x => x ∈ t) s)) / ↑(Finset.card s)
[PROOFSTEP]
simp only [div_eq_mul_inv, Finset.sum_const, nsmul_eq_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Nonempty α
a : α
⊢ ↑(uniformOfFintype α) a = (↑(Fintype.card α))⁻¹
[PROOFSTEP]
simp [uniformOfFintype, Finset.mem_univ, if_true, uniformOfFinset_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Nonempty α
a : α
⊢ Finset.card Finset.univ = Fintype.card α
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α✝
inst✝² : Nonempty α✝
α : Type u_4
inst✝¹ : Fintype α
inst✝ : Nonempty α
x : α
⊢ x ∈ support (uniformOfFintype α) ↔ x ∈ ⊤
[PROOFSTEP]
simp [mem_support_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Nonempty α
a : α
⊢ a ∈ support (uniformOfFintype α)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Nonempty α
s : Set α
⊢ ↑(toOuterMeasure (uniformOfFintype α)) s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)
[PROOFSTEP]
rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_ofFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Nonempty α
s : Set α
⊢ ↑(Finset.card (Finset.filter (fun x => x ∈ s) Finset.univ)) / ↑(Finset.card Finset.univ) =
    ↑(Finset.card (Finset.filter (fun x => x ∈ s) Finset.univ)) / ↑(Fintype.card α)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
inst✝¹ : Nonempty α
s : Set α
inst✝ : MeasurableSpace α
hs : MeasurableSet s
⊢ ↑↑(toMeasure (uniformOfFintype α)) s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)
[PROOFSTEP]
simp [uniformOfFintype, hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
inst✝¹ : Nonempty α
s : Set α
inst✝ : MeasurableSpace α
hs : MeasurableSet s
⊢ ↑(Finset.card (Finset.filter (fun x => x ∈ s) Finset.univ)) / ↑(Finset.card Finset.univ) =
    ↑(Finset.card (Finset.filter (fun x => x ∈ s) Finset.univ)) / ↑(Fintype.card α)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
⊢ ∑' (b : α), ↑(Multiset.count b s) / ↑(↑Multiset.card s) = (↑(↑Multiset.card s))⁻¹ * ∑' (b : α), ↑(Multiset.count b s)
[PROOFSTEP]
simp_rw [ENNReal.div_eq_inv_mul, ENNReal.tsum_mul_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
a : α
ha : ¬a ∈ Multiset.toFinset s
⊢ Multiset.count a s = 0
[PROOFSTEP]
rwa [Multiset.count_eq_zero, ← Multiset.mem_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
⊢ (↑(↑Multiset.card s))⁻¹ * ∑ b in Multiset.toFinset s, ↑(Multiset.count b s) = 1
[PROOFSTEP]
rw [← Nat.cast_sum, Multiset.toFinset_sum_count_eq s,
  ENNReal.inv_mul_cancel (Nat.cast_ne_zero.2 (hs ∘ Multiset.card_eq_zero.1)) (ENNReal.nat_ne_top _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
⊢ ∀ (x : α), x ∈ support (ofMultiset s hs) ↔ x ∈ ↑(Multiset.toFinset s)
[PROOFSTEP]
simp [mem_support_iff, hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
a : α
⊢ a ∈ support (ofMultiset s hs) ↔ a ∈ Multiset.toFinset s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
a : α
ha : ¬a ∈ s
⊢ ↑(ofMultiset s hs) a = 0
[PROOFSTEP]
simpa only [ofMultiset_apply, ENNReal.div_eq_zero_iff, Nat.cast_eq_zero, Multiset.count_eq_zero, ENNReal.nat_ne_top,
  or_false_iff] using ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ ↑(toOuterMeasure (ofMultiset s hs)) t =
    (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s))) / ↑(↑Multiset.card s)
[PROOFSTEP]
simp_rw [div_eq_mul_inv, ← ENNReal.tsum_mul_right, toOuterMeasure_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ ∑' (x : α), Set.indicator t (↑(ofMultiset s hs)) x =
    ∑' (i : α), ↑(Multiset.count i (Multiset.filter (fun x => x ∈ t) s)) * (↑(↑Multiset.card s))⁻¹
[PROOFSTEP]
refine' tsum_congr fun x => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
⊢ Set.indicator t (↑(ofMultiset s hs)) x =
    ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s)) * (↑(↑Multiset.card s))⁻¹
[PROOFSTEP]
by_cases hx : x ∈ t
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
hx : x ∈ t
⊢ Set.indicator t (↑(ofMultiset s hs)) x =
    ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s)) * (↑(↑Multiset.card s))⁻¹
[PROOFSTEP]
simp [Set.indicator, hx, div_eq_mul_inv]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
hx : ¬x ∈ t
⊢ Set.indicator t (↑(ofMultiset s hs)) x =
    ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s)) * (↑(↑Multiset.card s))⁻¹
[PROOFSTEP]
simp [Set.indicator, hx, div_eq_mul_inv]
