Typeclasses for Denotational Monad Semantics #
The primary distribution evalDist is a Mathlib Measure. The explicit evalSPMF / 𝒮[…]
surface remains available for finite executable distributions, and probOutput, probEvent, and
probFailure are discrete scalar adapters with theorems stating their meaning in evalDist.
-- dtumad: document various probability notation definitions here
Discrete probability lifts #
Support comes from MonadAttach. Discrete probability uses direct MonadLiftT declarations
to keep instance resolution stable for parameterized carriers. Lifts whose source is
parameterized (OracleComp spec, OptionT m, StateT σ m, …) and
which are gated by a typeclass on the parameter ([IsProbabilitySpec spec],
[MonadLiftT m SPMF], …) must also be MonadLiftT, not MonadLift. Demoting
to MonadLift forces Lean to find the instance through its transitive
instance, whose outer hop is MonadLift n o with n a semiOutParam. When
the recursion lands on a parameterized head like MonadLift (OracleComp ?spec) PMF,
Lean has to simultaneously unify ?spec through the semiOutParam, discharge
the typeclass premise on ?spec, and pin down ?spec from the inner reflexive
premise — a combination Lean's instance search refuses to chase. The direct
MonadLiftT declaration sidesteps this with a single-step head match.
Coherence between support (via MonadAttach) and evalSPMF
(via MonadLiftT m SPMF): x ∈ support mx iff Pr[= x | mx] ≠ 0.
This typeclass records agreement of attachment support with discrete probability outputs,
i.e. support mx = SPMF.support (evalSPMF mx).
The reachable outputs of
mx(viasupport) are exactly the outputs with nonzero probability inevalSPMF mx.
Instances
Evaluation distribution notation for any monad lifting into SPMF.
Instances For
The whole-denotation unfolding of the compatibility adapter.
The theorem has only the legacy MonadLiftT m SPMF assumption, so the measure on the left is
the adapter instance defined in Defs.Measure; a measure-native semantics is reasoned about
through the DiscreteEvalDistCompatible bridges instead of being converted back to an SPMF.
Probability that a computation mx returns the value x.
This remains definitionally the point mass of the executable SPMF semantics;
evalDist_apply_singleton is the equivalent measure-level reading.
Instances For
Probability that a computation mx outputs a value satisfying p.
The traditional notation remains the executable SPMF event API and is therefore usable for
arbitrary predicates. General measure developments should apply 𝒟[mx] to a measurable event;
evalDist_apply_setOf bridges the two on discrete spaces.
Instances For
Probability that a computation mx will fail to return a value.
Instances For
Probability that a computation returns a particular output.
Instances For
Probability that a computation returns a value satisfying a predicate.
Instances For
Probability that a computation fails to return a value.
Instances For
Alias of the reverse direction of probOutput_eq_zero_iff.
Alias of the forward direction of probOutput_eq_zero_iff.
Alias of the reverse direction of zero_eq_probOutput_iff.
Alias of the forward direction of probOutput_eq_zero_iff'.
Alias of the reverse direction of probOutput_eq_zero_iff'.
Alias of the reverse direction of zero_eq_probOutput_iff'.
Alias of the reverse direction of probOutput_pos_iff.
Alias of the forward direction of probOutput_pos_iff.
Alias of the forward direction of probOutput_pos_iff'.
Alias of the reverse direction of probOutput_pos_iff'.
Alias of the reverse direction of probEvent_eq_zero_iff.
Alias of the reverse direction of probEvent_eq_zero_iff'.
Alias of the reverse direction of probEvent_ne_zero_iff.
Alias of the reverse direction of probEvent_ne_zero_iff'.
Alias of the reverse direction of probEvent_pos_iff.
Alias of the reverse direction of probEvent_pos_iff'.
Set.Nonempty companion to the named rewrite probEvent_ne_zero_iff: the event has positive
probability iff some reachable output satisfies p. The Set.Nonempty witness stays atomic under
grind (unlike the saturating ∃ x ∈ support mx, p x form). Mirrors
probFailure_eq_one_iff_not_nonempty.
Deliberately NOT in the default grind set: together with probEvent_eq_zero_iff_not_nonempty
and probFailure_eq_one_iff_not_nonempty it re-forms a saturation cycle in the generic-monad
context (grind times out on the probEvent_eq_one_iff statement shape with all three tagged;
dropping any one of the trio restores fail-fast, and dropping this one is free: grind recovers
≠ 0 ↔ Nonempty from the kept = 0 ↔ ¬ Nonempty sibling by classical negation). Gated by
VCVioTest/GrindFailFast.lean.
grind-friendly companion to the simp-only probEvent_eq_zero_iff: the event has probability
zero iff no reachable output satisfies p, phrased via Set.Nonempty rather than the saturating
∀ x ∈ support mx, ¬ p x. The negation of probEvent_ne_zero_iff_nonempty.
If two events are equivalent on the support of mx then they have the same output chance.
Probability that a computation returns a value satisfying a predicate.
Instances For
Probability bounds and total-probability sums #
Alias of the reverse direction of probOutput_eq_one_iff.
Alias of the reverse direction of one_eq_probOutput_iff.
Alias of the reverse direction of probOutput_eq_one_iff'.
Alias of the reverse direction of one_eq_probOutput_iff'.
If a non-failing computation can only return x, then it returns x with probability one.
grind-friendly companion to probFailure_eq_one_iff: phrasing "fails with probability one"
via Set.Nonempty — which grind keeps atomic — avoids the support quantifier that makes the
support = ∅ form saturate, so this stays in the default grind set.
Lemmas for monads with a total PMF denotation #
These lemmas hold when m lifts into PMF (so computations never fail). They expose the
absence of failure mass and total normalization of the resulting distribution.
First-moment / Markov bound. The probability of p is at most the expectation of any
ℝ≥0∞-valued cost c that is ≥ 1 wherever p holds. This is the elementary core of a
first-moment (union) argument: a monotone "bad" event whose occurrence forces a unit of some
nonnegative cost has probability bounded by the expected cost.
First-moment / Markov bound (support-restricted cost). Variant of
probEvent_le_tsum_probOutput_mul_cost whose c ≥ 1 hypothesis need only hold on the
support of mx.
If p implies q on the support of a computation then it is more likely to happen.
If p implies q on the finSupport of a computation then it is more likely to happen.
If p implies q everywhere then p is less likely than q. Convenience
specialisation of probEvent_mono that drops the support hypothesis.
Alias of the reverse direction of probEvent_eq_one_iff.
Pointwise variant of probOutput_eq_one_iff: Pr[= x | mx] = 1 iff the support is
a subset of {x} (phrased as a forall over the support) and the computation never fails.
More usable than probOutput_eq_one_iff when the caller wants to iterate over arbitrary
support elements rather than prove a set equality.
Alias of the reverse direction of one_eq_probEvent_iff.
Alias of the reverse direction of probEvent_eq_one_iff'.
Alias of the reverse direction of one_eq_probEvent_iff'.
Expected values #
The expected value ∑' x, Pr[= x | mx] * g x of g on the output of mx. Failing runs
contribute nothing, so on a computation that can fail this is the expectation of the
conditional-on-success value scaled by the success probability, not a conditional expectation.
expectedValue is the head symbol gcongr keys on for bind bounds (see
probEvent_bind_eq_expectedValue).
Instances For
Expectation is monotone in the functional. Tagged at low gcongr priority so that
expectedValue_mono_of_support, which only asks for the bound on support mx, is tried first.
A pointwise bound on the functional bounds the expectation, since the total mass is at most one.
The expectation of an indicator is the event probability.
A constant factor scales the expectation.
expectedValue_mono with the hypothesis restricted to support mx. After gcongr with x hx
the goal is g x ≤ h x with hx : x ∈ support mx in context.
A bound on the functional over support mx bounds the expectation.
Functionals that agree on support mx have the same expectation.
The measure-to-façade bridge #
DiscreteEvalDistCompatible is the one fact that connects the primary measure semantics to the
discrete façade: integrating a measurable functional against 𝒟[mx] is the mass-weighted sum
∑' x, Pr[= x | mx] * g x. Every singleton, event and mass bridge below derives from it, so the
measure side reduces into the façade, where the simp/grind contract takes over, instead of
carrying a second family of sum lemmas. The compatibility adapter satisfies it definitionally;
the free-monad fold satisfies it whenever its measure specification agrees with the probability
specification (PFunctor.IsMeasureSpec.Compatible).
The SPMF layer behind the façade is transitional. This class and the lemmas derived from it are
the surface that survives the switch to measure-native definitions: once Pr[…] is defined from
𝒟[…] they become definitional, while the SPMF. glue that proves the adapter instance is what
that switch deletes.
The primary measure semantics agrees with the discrete façade: integrating a measurable
functional against 𝒟[mx] is the façade expectation ∑' x, Pr[= x | mx] * g x.
- lintegral_evalDist {α : Type u} [MeasurableSpace α] (mx : m α) {g : α → ENNReal} (hg : Measurable g) : ∫⁻ (x : α), g x ∂𝒟[mx] = ∑' (x : α), Pr[= x | mx] * g x
Integrals against the denoted measure are mass-weighted sums over the façade.
Instances
The compatibility adapter denotes (𝒮[mx]).toMeasure, so the bridge is
SPMF.lintegral_toMeasure. Stated with only the lift in scope, so the semantics instance is
the adapter itself.
The measure of a measurable event is the façade probability of membership.
Singleton mass is the point probability.
Native observed events agree with the scalar compatibility surface under explicit coherence.
On a discrete space the measure of a predicate's event is its façade probability.
Success mass is one minus the failure probability.
Reachable outputs are exactly the positive-mass singletons. General measures can have support points of mass zero, so the statement is deliberately restricted to singleton-measurable spaces.