From 0462759e222f3b725a7200d723ce7ebc6b99622a Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 23:43:54 +0000 Subject: [PATCH] Improve MeasurableSpaceMonad Documentation --- RandomDo/Monad/MeasurableSpace.lean | 88 +++++++++++++++++++++++------ 1 file changed, 70 insertions(+), 18 deletions(-) diff --git a/RandomDo/Monad/MeasurableSpace.lean b/RandomDo/Monad/MeasurableSpace.lean index b593969..eb2ebfe 100644 --- a/RandomDo/Monad/MeasurableSpace.lean +++ b/RandomDo/Monad/MeasurableSpace.lean @@ -9,19 +9,48 @@ public import Mathlib.Control.Random public import Mathlib.MeasureTheory.Measure.GiryMonad /-! -# Measurable Space Monad +# Measurable space monads -**TODO** +This file defines `MeasurableSpaceFunctor` and `MeasurableSpaceMonad` as classes on functions of +the form `m : (α : Type u) → [MeasurableSpace α] → Type v`. They play the role of Lean core's +`Functor` and `Monad` for types equipped with a `MeasurableSpace` instance. Assuming that instances +are lawful, this corresponds to functors and monads on the category of measurable spaces. ## Main definitions -* `MeasurableSpaceFunctor f`: **TODO** -* `MeasurableSpaceMonad m`: **TODO** -* `LawfulMeasurableSpaceFunctor f`: **TODO** -* `LawfulMeasurableSpaceMonad m`: **TODO** +* `MeasurableSpaceFunctor`: A typeclass for functors on types equipped with a `MeasurableSpace` +instance. +* `MeasurableSpaceMonad`: A typeclass for monads on types equipped with a `MeasurableSpace` +instance. +* `LawfulMeasurableSpaceFunctor`: A `Prop`-valued typeclass which states that a given +`MeasurableSpaceFunctor` satisfies the laws of a functor on measurable spaces. +* `LawfulMeasurableSpaceMonad`: A `Prop`-valued typeclass which states that a given +`MeasurableSpaceMonad` satisfies the laws of a monad on measurable spaces. * `MeasurableSpaceForIn`: **TODO** * `MeasurableSpaceForIn'`: **TODO** +## Notation + +The following notation is available: + +* `f <$>ₘ x`: `MeasurableSpaceFunctor.mMap f x`. +* `x >>=ₘ f`: `MeasurableSpaceBind.mBind x f`. + +## Implementation details + +The development of `MeasurableSpaceMonad` mirrors the development of `Monad` in Lean core, including +the definition of intermediate classes `MeasurableSpaceFunctor`, `MeasurableSpacePure`, and +`MeasurableSpaceBind` except that there is no `MeasurableSpaceApplicative` and instead +`MeasurableSpaceMonad` extends all three of the preceding classes directly. This is because +defining a `MeasurableSpaceApplicative` would require defining an analogue of +`Seq.seq : m (α → β) → (Unit → m α) → m β`, and we would like such an operation to be jointly +measurable in `m (α → β)` and `Unit → m α`, but requiring this operation to be jointly measurable +would already fail for the identity monad: there, `seq f (fun _ => x) = f x`, so `seq` reduces to +function evaluation. No σ-algebra on the space of all measurable functions makes evaluation +jointly measurable in general; +see R. J. Aumann, [*Borel structures for function spaces*](https://doi.org/10.1215/ijm/1255631584), +*Illinois Journal of Mathematics* **5** (1961), no. 4, 614–630, §3. + -/ @[expose] public section @@ -34,25 +63,36 @@ universe u v section MeasurableSpaceMonad -/-- A functor on types with a `MeasurableSpace` instance. The `mMap` operator `<$>ₘ` is overloaded -via instances of this class. This class does not require proofs of the `MeasurableSpaceFunctor` -axioms. Proofs may be provided or required via the `LawfulMeasurableSpaceFunctor` class. -/ +/-- +A functor on types with a `MeasurableSpace` instance. This means a function +`f : (α : Type u) → [MeasurableSpace α] → Type v` equipped with an +`mMap [MeasurableSpace α] [MeasurableSpace β] : (α → β) → f α → f β` operator, +which can be written with the notation `<$>ₘ`. + +A lawful instance of this class requires a `MeasurableSpace` instance on each output type `f α`, +and that `mMap` maps measurable functions `α → β` to measurable functions `f α → f β`, maps +identity functions to identity functions, and respects composition of measurable functions. +This class does not require its instances to be lawful. Proofs of lawful instances can be +provided via the `Prop`-valued class `LawfulMeasurableSpaceFunctor`. + +Lawful instances of this class correspond to functors on the category of measurable spaces. +-/ class MeasurableSpaceFunctor (f : (α : Type u) → [MeasurableSpace α] → Type v) : Type (max (u+1) v) where /-- Applies a function inside a functor on measurable spaces. This is used to overload the `<$>ₘ` operator. - When mapping a constant function (if one cares about executing the code), use - `Functor.mMapConst` instead, because it may be more efficient. + When mapping a constant function in executable code, use + `MeasurableSpaceFunctor.mMapConst` instead, because it may be more efficient. -/ mMap {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : (α → β) → f α → f β /-- Mapping a constant function. Given `a : α` and `v : f β`, `mMapConst a v` is equivalent to `(fun _ => a) <$>ₘ v`. For some - functors, this can be implemented more efficiently; for all other functors, the default - implementation may be used. + functors where executable code is relevant, this can be implemented more efficiently; for all + other functors, the default implementation may be used. -/ mMapConst {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : α → f β → f α := mMap ∘ (const _) @@ -66,7 +106,7 @@ The `mPure` function is overloaded via `MeasurableSpacePure` instances. -/ class MeasurableSpacePure (f : (α : Type u) → [MeasurableSpace α] → Type v) where /-- Given `a : α` where `α` has a `MeasurableSpace` instance, `mPure a : f α` represents an - action that does nothing and returns a -/ + action that does nothing and returns `a`. -/ mPure {α : Type u} [MeasurableSpace α] : α → f α /-- @@ -85,8 +125,21 @@ class MeasurableSpaceBind (m : (α : Type u) → [MeasurableSpace α] → Type v @[inherit_doc] infixl:55 " >>=ₘ " => MeasurableSpaceBind.mBind -/-- A monad on types with a `MeasurableSpace` instance. This abstraction allows the user to write -code that depends on "random" side-effects -/ +/-- +A monad on types with a `MeasurableSpace` instance. + +Monads are an abstraction of sequential control flow and side effects in functional programming, +and `MeasurableSpaceMonad`s allow the use of this abstraction on programs taking values in +`MeasurableSpace`s. The canonical example of such a monad is `Measure` where programs +"written" in the `Measure` monad can represent programs with "random" outputs whose output +distribution is given by the output measure. `MeasurableSpaceMonad`s support `rdo` notation, +the measurable-space analogue of `do` notation, for specifying these programs. + +A lawful instance of this class should satisfy various properties so that the instance corresponds +to a monad on the category of measurable spaces. These are specified precisely in the `Prop`-valued +class `LawfulMeasurableSpaceMonad` and proofs of lawfulness can be given by defining an instance +of that class. +-/ class MeasurableSpaceMonad (m : (α : Type u) → [MeasurableSpace α] → Type v) : Type (max (u+1) v) extends MeasurableSpaceFunctor m, MeasurableSpacePure m, MeasurableSpaceBind m where @@ -159,8 +212,7 @@ class LawfulMeasurableSpaceMonad mBind_mPure_comp {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : Measurable f) (x : m α) : x >>=ₘ (fun a => mPure (f a)) = f <$>ₘ x - /-- `mPure` followed by `mBind` of a function application is equivalent to function - application. -/ + /-- Binding `mPure x` to a measurable function `f` is equivalent to applying `f` to `x`. -/ mPure_mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (x : α) {f : α → m β} (hf : Measurable f) : mPure x >>=ₘ f = f x