Improve MeasurableSpaceMonad Documentation

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