FintypePMF.normalize: normalize a positive weight vector

Canonical FintypePMF constructor from a strictly-positive weight function. The divisor is a Finset.sum, which makes the constructor a computable definition (noncomputable only because of the strict-positivity proof threading, not because of any upstream noncomputability).

noncomputable def ProbabilityTheory.FintypePMF.normalize {α : Type u_1} [Fintype α] [Nonempty α] (w : α → ℝ) (hw : ∀ (a : α), 0 < w a) : FintypePMF α

Normalize a strictly-positive weight vector to a FintypePMF.

Equations

• ProbabilityTheory.FintypePMF.normalize w hw = { prob := fun (a : α) => w a / ∑ a' : α, w a', prob_nonneg := ⋯, prob_sum_one := ⋯ }

theorem ProbabilityTheory.FintypePMF.normalize_prob {α : Type u_1} [Fintype α] [Nonempty α] (w : α → ℝ) (hw : ∀ (a : α), 0 < w a) (a : α) : (normalize w hw).prob a = w a / ∑ a' : α, w a'

(normalize w hw).prob a = w a / ∑ a', w a'.