Measure-valued evaluation and discrete compatibility

This module reexports VCVio.EvalDist.Defs.Measure.Core and supplies the discrete compatibility adapters. An EvalDistSemantics m interprets m α as a Mathlib Measure α with total mass at most one. Missing mass represents failure or nontermination. In particular, the output distribution itself does not introduce an Option outcome.

Measurable spaces are explicit arguments to the semantics. There is deliberately no blanket measurable-space instance for finite types: discrete adapters state their countability and measurability assumptions at the boundary where they are used.

LawfulPureEvalDistSemantics records the Giry pure law without imposing conditions on effects. LawfulEvalDistSemantics adds the bind law, keeping measurability of the continuation visible; evalDist_bind_of_discrete is the usual cryptographic specialization.

noncomputable def SPMF.toMeasure {α : Type u} [MeasurableSpace α] (p : SPMF α) : MeasureTheory.Measure α

Read an SPMF as the measure of its successful outputs. This is the explicit compatibility bridge from the finite executable backend to the primary measure API.

theorem SPMF.toMeasure_apply_univ_le_one {α : Type u} [MeasurableSpace α] (p : SPMF α) : p.toMeasure Set.univ ≤ 1

@[simp]

theorem SPMF.toMeasure_pure {α : Type u} [MeasurableSpace α] (x : α) : (pure x).toMeasure = MeasureTheory.Measure.dirac x

@[simp]

theorem SPMF.toMeasure_failure {α : Type u} [MeasurableSpace α] : failure.toMeasure = 0

Failure carries no successful-output mass.

@[simp]

theorem SPMF.toMeasure_apply_singleton {α : Type u} [MeasurableSpace α] (p : SPMF α) [MeasurableSingletonClass α] (x : α) : p.toMeasure {x} = p x

theorem SPMF.lintegral_toMeasure {α : Type u} [MeasurableSpace α] (p : SPMF α) {g : α → ENNReal} (hg : Measurable g) : ∫⁻ (x : α), g x ∂p.toMeasure = ∑' (x : α), p x * g x

Integrating a measurable function against the successful-output measure is the mass-weighted sum over successful outputs, with the mass on the left as in bind_apply_eq_tsum. This is the one place where the transitional option-valued backend meets Lebesgue integration; every singleton, event and expectation bridge derives from it, and it is the glue that disappears once the façade is defined from 𝒟[…] directly.

theorem SPMF.toMeasure_apply {α : Type u} [MeasurableSpace α] (p : SPMF α) {s : Set α} (hs : MeasurableSet s) : p.toMeasure s = ∑' (x : α), p x * s.indicator 1 x

The successful-output measure of a measurable set is the sum of the point masses it contains.

@[simp]

theorem SPMF.toMeasure_apply_univ {α : Type u} [MeasurableSpace α] (p : SPMF α) : p.toMeasure Set.univ = ∑' (x : α), p x

The total mass of the successful-output measure is the sum of the SPMF point masses.

theorem SPMF.toMeasure_injective {α : Type u} [MeasurableSpace α] [MeasurableSingletonClass α] : Function.Injective toMeasure

The successful-output measure retains the complete SPMF.

Failure mass is determined by the successful masses, so dropping the explicit none outcome does not lose information.

theorem SPMF.toMeasure_map {α : Type u} [MeasurableSpace α] (p : SPMF α) {β : Type u} [MeasurableSpace β] (f : α → β) (hf : Measurable f) : (f <$> p).toMeasure = MeasureTheory.Measure.map f p.toMeasure

The successful-output measure commutes with measurable maps.

theorem SPMF.toMeasure_bind' {α : Type u} [MeasurableSpace α] (p : SPMF α) {β : Type u} [MeasurableSpace β] (f : α → SPMF β) (hf : Measurable fun (x : α) => (f x).toMeasure) : (p >>= f).toMeasure = p.toMeasure.bind fun (x : α) => (f x).toMeasure

Successful-output measures commute with SPMF bind whenever the measure-valued continuation is measurable.

theorem SPMF.toMeasure_bind {α : Type u} [MeasurableSpace α] (p : SPMF α) {β : Type u} [DiscreteMeasurableSpace α] [MeasurableSpace β] (f : α → SPMF β) : (p >>= f).toMeasure = p.toMeasure.bind fun (x : α) => (f x).toMeasure

On a discrete source type every measure-valued continuation is measurable.

@[instance_reducible, instance 10]

noncomputable instance instEvalDistSemanticsOfMonadLiftTSPMF {m : Type u → Type v} [MonadLiftT m SPMF] : EvalDistSemantics m

Compatibility semantics for monads that still expose an SPMF lift.

The low priority lets a direct measure interpretation, such as the free-monad fold in PFunctorMeasure, win whenever both are available.

noncomputable def MeasureTheory.Measure.toSPMF {α : Type u} [MeasurableSpace α] [Countable α] [DiscreteMeasurableSpace α] (μ : Measure α) (hμ : μ Set.univ ≤ 1) : SPMF α

Convert a countable discrete subprobability measure to the compatibility SPMF backend.

The missing mass is first made explicit as none; the resulting probability measure can then use Mathlib's Measure.toPMF bridge.

@[simp]

theorem MeasureTheory.Measure.toSPMF_apply {α : Type u} [MeasurableSpace α] [Countable α] [DiscreteMeasurableSpace α] (μ : Measure α) (hμ : μ Set.univ ≤ 1) (x : α) : (μ.toSPMF hμ) x = μ {x}

theorem MeasureTheory.Measure.toSPMF_apply_none {α : Type u} [MeasurableSpace α] [Countable α] [DiscreteMeasurableSpace α] (μ : Measure α) (hμ : μ Set.univ ≤ 1) : (OptionT.run (μ.toSPMF hμ)) none = 1 - μ Set.univ

@[simp]

theorem MeasureTheory.Measure.toSPMF_toMeasure {α : Type u} [MeasurableSpace α] [Countable α] [DiscreteMeasurableSpace α] (μ : Measure α) (hμ : μ Set.univ ≤ 1) : (μ.toSPMF hμ).toMeasure = μ

Converting a discrete subprobability measure to SPMF and back preserves the measure.

@[simp]

theorem SPMF.toMeasure_toSPMF {α : Type u} [MeasurableSpace α] [Countable α] [DiscreteMeasurableSpace α] (p : SPMF α) : p.toMeasure.toSPMF ⋯ = p

Converting an SPMF to its successful-output measure and back preserves the SPMF.