From 89592a01acbe733a29bf9226692101233b1bc371 Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Fri, 13 Nov 2026 20:46:57 +0000 Subject: [PATCH 1/2] Export measurable monad operations and laws --- RandomDo/MeasurableSpaceMonad/Defs.lean | 16 +++++++++------- RandomDo/Monad/ForInInstances.lean | 2 +- RandomDo/Monad/Instances.lean | 6 ++---- RandomDo/Monad/Notation.lean | 2 +- RandomDo/Tactic/IsMarkov/Lemmas.lean | 1 - Test/MonadLaws.lean | 3 +-- 6 files changed, 14 insertions(+), 16 deletions(-) diff --git a/RandomDo/MeasurableSpaceMonad/Defs.lean b/RandomDo/MeasurableSpaceMonad/Defs.lean index 940bce5..af9292c 100644 --- a/RandomDo/MeasurableSpaceMonad/Defs.lean +++ b/RandomDo/MeasurableSpaceMonad/Defs.lean @@ -107,6 +107,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`. @@ -121,6 +123,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 /-- @@ -158,8 +162,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] @@ -169,7 +171,8 @@ class LawfulMeasurableSpaceFunctor {g : α → β} (hg : Measurable g) : Measurable ((g <$>ₘ ·) : f α → f β) /-- The `mMapConst` implementation is equivalent to the default implementation. -/ mMap_const {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : - (mMapConst : α → f β → f α) = mMap ∘ const β + (MeasurableSpaceFunctor.mMapConst : α → f β → f α) = + MeasurableSpaceFunctor.mMap ∘ const β /-- `mMap` preserves identity. -/ id_mMap {α : Type u} [MeasurableSpace α] (x : f α) : id <$>ₘ x = x /-- `mMap` preserves function composition of measurable functions. -/ @@ -177,7 +180,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 @@ -193,8 +196,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] @@ -227,7 +228,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 diff --git a/RandomDo/Monad/ForInInstances.lean b/RandomDo/Monad/ForInInstances.lean index fde7c94..9a0cfc7 100644 --- a/RandomDo/Monad/ForInInstances.lean +++ b/RandomDo/Monad/ForInInstances.lean @@ -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} diff --git a/RandomDo/Monad/Instances.lean b/RandomDo/Monad/Instances.lean index e716032..5b9a4c4 100644 --- a/RandomDo/Monad/Instances.lean +++ b/RandomDo/Monad/Instances.lean @@ -36,16 +36,14 @@ 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 mBind := Measure.bind instance : LawfulMeasurableSpaceMonad Measure where - mMap_const := by simp [mMapConst, mMap] - id_mMap μ := by simp [mMap] + mMap_const := by simp [MeasurableSpaceFunctor.mMapConst, MeasurableSpaceFunctor.mMap] + id_mMap μ := by simp [MeasurableSpaceFunctor.mMap] measurable_mPure := by unfold mPure; fun_prop measurable_mBind := by unfold mBind; fun_prop mBind_mPure_comp _ _ := by rfl diff --git a/RandomDo/Monad/Notation.lean b/RandomDo/Monad/Notation.lean index 9b1d5f9..672bc78 100644 --- a/RandomDo/Monad/Notation.lean +++ b/RandomDo/Monad/Notation.lean @@ -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 diff --git a/RandomDo/Tactic/IsMarkov/Lemmas.lean b/RandomDo/Tactic/IsMarkov/Lemmas.lean index 38cc0d0..7a496a7 100644 --- a/RandomDo/Tactic/IsMarkov/Lemmas.lean +++ b/RandomDo/Tactic/IsMarkov/Lemmas.lean @@ -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 diff --git a/Test/MonadLaws.lean b/Test/MonadLaws.lean index 7787395..fa84ce8 100644 --- a/Test/MonadLaws.lean +++ b/Test/MonadLaws.lean @@ -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 From ac268a78abe0427ef1f39894d8b5d6032e94c03b Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Fri, 13 Nov 2026 21:08:50 +0000 Subject: [PATCH 2/2] Export measurable functor operations --- RandomDo/MeasurableSpaceMonad/Defs.lean | 5 +++-- RandomDo/Monad/Instances.lean | 4 ++-- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/RandomDo/MeasurableSpaceMonad/Defs.lean b/RandomDo/MeasurableSpaceMonad/Defs.lean index af9292c..74d5fc8 100644 --- a/RandomDo/MeasurableSpaceMonad/Defs.lean +++ b/RandomDo/MeasurableSpaceMonad/Defs.lean @@ -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 /-- @@ -171,8 +173,7 @@ class LawfulMeasurableSpaceFunctor {g : α → β} (hg : Measurable g) : Measurable ((g <$>ₘ ·) : f α → f β) /-- The `mMapConst` implementation is equivalent to the default implementation. -/ mMap_const {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : - (MeasurableSpaceFunctor.mMapConst : α → f β → f α) = - MeasurableSpaceFunctor.mMap ∘ const β + (mMapConst : α → f β → f α) = mMap ∘ const β /-- `mMap` preserves identity. -/ id_mMap {α : Type u} [MeasurableSpace α] (x : f α) : id <$>ₘ x = x /-- `mMap` preserves function composition of measurable functions. -/ diff --git a/RandomDo/Monad/Instances.lean b/RandomDo/Monad/Instances.lean index 5b9a4c4..04bf7c3 100644 --- a/RandomDo/Monad/Instances.lean +++ b/RandomDo/Monad/Instances.lean @@ -42,8 +42,8 @@ noncomputable instance : MeasurableSpaceMonad Measure where mBind := Measure.bind instance : LawfulMeasurableSpaceMonad Measure where - mMap_const := by simp [MeasurableSpaceFunctor.mMapConst, MeasurableSpaceFunctor.mMap] - id_mMap μ := by simp [MeasurableSpaceFunctor.mMap] + mMap_const := by simp [mMapConst, mMap] + id_mMap μ := by simp [mMap] measurable_mPure := by unfold mPure; fun_prop measurable_mBind := by unfold mBind; fun_prop mBind_mPure_comp _ _ := by rfl