Measure semantics for applicative sequencing

Independent applicative pairs denote Mathlib product measures on arbitrary measurable spaces. Discarding either output retains the successful mass of its computation as a scaling factor. No operational support, discrete evaluator, or measurable structure on a function space is needed.

@[simp]

theorem evalDist_seq_map_prod_mk {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (my : m β) : 𝒟[Prod.mk <$> mx <*> my] = 𝒟[mx].prod 𝒟[my]

Independently sampled applicative pairs have the product of their output measures.

theorem evalDist_seq_map {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (mx : m α) (my : m β) (f : α → β → γ) (hf : Measurable (Function.uncurry f)) : 𝒟[f <$> mx <*> my] = MeasureTheory.Measure.map (Function.uncurry f) (𝒟[mx].prod 𝒟[my])

An applicative binary operation pushes its product law forward along the uncurried operation. Only that operation's joint measurability is needed, without a measurable function space.

@[simp]

theorem evalDist_seqLeft {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (my : m β) : 𝒟[mx <* my] = 𝒟[my] Set.univ • 𝒟[mx]

Keeping the first result scales its measure by the second computation's successful mass.

@[simp]

theorem evalDist_seqRight {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (my : m β) : 𝒟[mx *> my] = 𝒟[mx] Set.univ • 𝒟[my]

Keeping the second result scales its measure by the first computation's successful mass.

@[simp]

theorem evalDist_map_seqLeft {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β γ : Type u} [MeasurableSpace β] [MeasurableSpace γ] (mx : m α) (my : m β) (f : α → γ) : 𝒟[f <$> (mx <* my)] = 𝒟[my] Set.univ • 𝒟[f <$> mx]

Mapping the retained first output commutes with discarding the second output. No measurable space or measurability obligation is needed for the intermediate first output.

@[simp]

theorem evalDist_map_seqRight {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace γ] (mx : m α) (my : m β) (f : β → γ) : 𝒟[f <$> (mx *> my)] = 𝒟[mx] Set.univ • 𝒟[f <$> my]

Mapping the retained second output commutes with discarding the first output. No measurable space or measurability obligation is needed for the intermediate second output.

instance evalDist.instIsProbabilityMeasureSeqMapProdMk {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (my : m β) [MeasureTheory.IsProbabilityMeasure 𝒟[mx]] [MeasureTheory.IsProbabilityMeasure 𝒟[my]] : MeasureTheory.IsProbabilityMeasure 𝒟[Prod.mk <$> mx <*> my]

An independent applicative pair inherits losslessness from its factors.

instance evalDist.instIsProbabilityMeasureSeqLeft {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (my : m β) [MeasureTheory.IsProbabilityMeasure 𝒟[mx]] [MeasureTheory.IsProbabilityMeasure 𝒟[my]] : MeasureTheory.IsProbabilityMeasure 𝒟[mx <* my]

Keeping the first of two lossless computations preserves its probability certificate.

instance evalDist.instIsProbabilityMeasureSeqRight {m : Type u → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (my : m β) [MeasureTheory.IsProbabilityMeasure 𝒟[mx]] [MeasureTheory.IsProbabilityMeasure 𝒟[my]] : MeasureTheory.IsProbabilityMeasure 𝒟[mx *> my]

Keeping the second of two lossless computations preserves its probability certificate.

theorem prEvent_seqLeft {m : Type → Type v'} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} [MeasurableSpace β] (mx : m α) (my : m β) (p : α → Prop) : 𝒟[do let x ← mx <* my pure (p x)] {True} = 𝒟[my] Set.univ * 𝒟[do let x ← mx pure (p x)] {True}

A final event about the first result retains the second computation's successful mass. The retained result type needs no measurable-space argument.

theorem prEvent_seqRight {m : Type → Type v'} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} [MeasurableSpace α] (mx : m α) (my : m β) (p : β → Prop) : 𝒟[do let y ← mx *> my pure (p y)] {True} = 𝒟[mx] Set.univ * 𝒟[do let y ← my pure (p y)] {True}

A final event about the second result retains the first computation's successful mass. The retained result type needs no measurable-space argument.