FintypePMF.pointMass: Dirac point-mass PMF on a single element

Given a distinguished a₀ : α, pointMass a₀ puts all the weight on a₀. Used by the covering-row argument in Probability/Decision/Minimax/.

def ProbabilityTheory.FintypePMF.pointMass {α : Type u_1} [Fintype α] [DecidableEq α] (a₀ : α) : FintypePMF α

Point-mass FintypePMF at a fixed element a₀.

Equations

• ProbabilityTheory.FintypePMF.pointMass a₀ = { prob := fun (a : α) => if a = a₀ then 1 else 0, prob_nonneg := ⋯, prob_sum_one := ⋯ }