FintypePMF.empirical: empirical distribution of a finite sequence

Given a length-T sequence rs : Fin T → α, the empirical PMF puts weight (count of a in rs) / T on each a. Used to turn an MWU row sequence into a row mixture.

noncomputable def ProbabilityTheory.FintypePMF.empirical {α : Type u_1} [Fintype α] [DecidableEq α] {T : ℕ} (hT : 0 < T) (rs : Fin T → α) : FintypePMF α

Empirical FintypePMF from a length-T sequence.

Equations

• ProbabilityTheory.FintypePMF.empirical hT rs = { prob := fun (a : α) => ↑{t : Fin T | rs t = a}.card / ↑T, prob_nonneg := ⋯, prob_sum_one := ⋯ }