Skip to content

Export measurable monad operations and laws #25

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
DavidLedvinka wants to merge 2 commits into
base: main
Choose a base branch
from
+12 −13
Open

Export measurable monad operations and laws #25

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
89592a0
Export measurable monad operations and laws
Nov 13, 2026
ac268a7
Export measurable functor operations
Nov 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 9 additions & 6 deletions RandomDo/MeasurableSpaceMonad/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,6 +95,8 @@ class MeasurableSpaceFunctor (f : (α : Type u) → [MeasurableSpace α] → Typ
mMapConst {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : α → f β → f α :=
mMap ∘ (const _)

export MeasurableSpaceFunctor (mMap mMapConst)

@[inherit_doc] scoped infixr:100 " <$>ₘ " => MeasurableSpaceFunctor.mMap

/--
Expand All @@ -107,6 +109,8 @@ class MeasurableSpacePure (f : (α : Type u) → [MeasurableSpace α] → Type v
action that does nothing and returns `a`. -/
mPure {α : Type u} [MeasurableSpace α] : α → f α

export MeasurableSpacePure (mPure)

/--
The `>>=ₘ` operator is overloaded via instances of `MeasurableSpaceBind`.

Expand All @@ -121,6 +125,8 @@ class MeasurableSpaceBind (m : (α : Type u) → [MeasurableSpace α] → Type v
-/
mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : m α → (α → m β) → m β

export MeasurableSpaceBind (mBind)

@[inherit_doc] scoped infixl:55 " >>=ₘ " => MeasurableSpaceBind.mBind

/--
Expand Down Expand Up @@ -158,8 +164,6 @@ end MeasurableSpaceMonad

section Lawful

open MeasurableSpaceFunctor

/-- A `MeasurableSpaceFunctor` satisfies the measurable space functor laws. -/
class LawfulMeasurableSpaceFunctor
(f : (α : Type u) → [MeasurableSpace α] → Type v) [MeasurableSpaceFunctor f]
Expand All @@ -177,7 +181,7 @@ class LawfulMeasurableSpaceFunctor
{g₀ : α → β} {g₁ : β → γ} (x : f α) (hg₀ : Measurable g₀) (hg₁ : Measurable g₁) :
(g₁ ∘ g₀) <$>ₘ x = g₁ <$>ₘ g₀ <$>ₘ x

open LawfulMeasurableSpaceFunctor
export LawfulMeasurableSpaceFunctor (measurable_mMap mMap_const id_mMap comp_mMap)

attribute [fun_prop] measurable_mMap
attribute [simp] id_mMap
Expand All @@ -193,8 +197,6 @@ variable {f : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpac
g₁ <$>ₘ g₀ <$>ₘ x = (fun a => g₁ (g₀ a)) <$>ₘ x :=
(comp_mMap x hg₀ hg₁).symm

open MeasurableSpaceBind MeasurableSpacePure MeasurableSpaceFunctor

/-- A `MeasurableSpaceMonad` satisfies the measurable space monad laws. -/
class LawfulMeasurableSpaceMonad
(m : (α : Type u) → [MeasurableSpace α] → Type v) [MeasurableSpaceMonad m]
Expand Down Expand Up @@ -227,7 +229,8 @@ class LawfulMeasurableSpaceMonad
congr with _
exact (mPure_mBind _ (measurable_mPure.comp h_meas)).symm)

open LawfulMeasurableSpaceMonad
export LawfulMeasurableSpaceMonad
(measurable_mPure measurable_mBind mBind_mPure_comp mPure_mBind mBind_assoc)

attribute [fun_prop] measurable_mPure measurable_mBind
attribute [simp] mPure_mBind mBind_assoc mBind_mPure_comp
Expand Down
2 changes: 1 addition & 1 deletion RandomDo/Monad/ForInInstances.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ end MeasurableSpace

universe u v

open MeasureTheory MeasurableSpacePure
open MeasureTheory

variable {α : Type u} [mα : MeasurableSpace α] {m : (α : Type u) → [MeasurableSpace α] → Type v}

Expand Down
2 changes: 0 additions & 2 deletions RandomDo/Monad/Instances.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,6 @@ instance {m : Type u → Type v} [Monad m] :
/-- A measurable space monad for pseudo random number generation. -/
abbrev PseudoRandomM := Monad.toMeasurableSpaceMonad Rand

open MeasurableSpacePure MeasurableSpaceBind MeasurableSpaceFunctor MeasurableSpaceMonad

@[simps]
noncomputable instance : MeasurableSpaceMonad Measure where
mPure := Measure.dirac
Expand Down
2 changes: 1 addition & 1 deletion RandomDo/Monad/Notation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ public meta import Lean.Meta.ProdN

open Lean Lean.Parser Lean.Parser.Term Lean.Meta Lean.Elab Lean.Elab.Do Lean.Elab.Term Std Meta

open MeasureTheory MeasurableSpacePure MeasurableSpaceBind
open MeasureTheory

public meta section

Expand Down
1 change: 0 additions & 1 deletion RandomDo/Tactic/IsMarkov/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,6 @@ complex program to the Markov property/measurability of its underlying mathemati
@[expose] public section

open MeasureTheory ProbabilityTheory Function
open MeasurableSpacePure
open scoped ENNReal

namespace IsMarkov
Expand Down
3 changes: 1 addition & 2 deletions Test/MonadLaws.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,7 @@ guarded by measurability hypotheses, which is what makes the Giry monad fit the
these tests also record the exact shape each law is stated in.
-/

open MeasureTheory ProbabilityTheory MeasurableSpacePure MeasurableSpaceBind
MeasurableSpaceFunctor
open MeasureTheory ProbabilityTheory

@[expose] public section

Expand Down
Loading