EvalDist Instances for FinRatPMF.Raw

This file exposes the executable FinRatPMF.Raw monad to the generic EvalDist API.

@[implicit_reducible]

noncomputable instance FinRatPMF.Raw.instMonadLiftPMF_vCVio : MonadLift Raw PMF

instance FinRatPMF.Raw.instLawfulMonadLiftPMF_vCVio : LawfulMonadLift Raw PMF

@[implicit_reducible]

noncomputable instance FinRatPMF.Raw.instMonadLiftTRawSetM : MonadLiftT Raw SetM

Direct MonadLiftT Raw SetM defined via the underlying PMF support. The generic MonadLiftT SPMF SetM is non-transitive (declared as MonadLiftT, not MonadLift, so monadLiftTrans cannot chain through it), so every monad with probabilistic semantics declares its SetM lift directly.

instance FinRatPMF.Raw.instLawfulMonadLiftTRawSetM : LawfulMonadLiftT Raw SetM

instance FinRatPMF.Raw.instEvalDistCompatible : EvalDistCompatible Raw

Compatibility: Raw's SetM support equals the SPMF support of its evalDist.

@[implicit_reducible]

instance FinRatPMF.Raw.instHasEvalFinset : HasEvalFinset Raw

@[simp]

theorem FinRatPMF.Raw.finSupport_eq_support {α : Type u} [DecidableEq α] (mx : Raw α) : finSupport mx = mx.support