Strictly-positive-prior typeclass

HasPositivePrior P certifies that every weight of the FintypePMF P is strictly positive. Useful for divergence computations where log(0/·) conventions would otherwise need case-splits.

class ProbabilityTheory.FintypePMF.HasPositivePrior {α : Type u_1} [Fintype α] (P : FintypePMF α) : Prop

A FintypePMF with strictly positive weights on every element.

• pos (a : α) : 0 < P.prob a