feat: notations to specify sigma algebras for integrability, measures…

… and kernels (#15316) from GibbsMeasure Co-authored-by: Yael Dillies <[email protected]>
leanprover-community · Sep 11, 2024 · 539f732 · 539f732
1 parent 506c762
commit 539f732
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 1 deletion.
diff --git a/Mathlib/MeasureTheory/Function/L1Space.lean b/Mathlib/MeasureTheory/Function/L1Space.lean
@@ -389,6 +389,9 @@ end NormedSpace
 def Integrable {α} {_ : MeasurableSpace α} (f : α → β) (μ : Measure α := by volume_tac) : Prop :=
   AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ
 
+/-- Notation for `Integrable` with respect to a non-standard σ-algebra. -/
+scoped notation "Integrable[" mα "]" => @Integrable _ _ _ mα
+
 theorem memℒp_one_iff_integrable {f : α → β} : Memℒp f 1 μ ↔ Integrable f μ := by
   simp_rw [Integrable, HasFiniteIntegral, Memℒp, eLpNorm_one_eq_lintegral_nnnorm]
 

diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Defs.lean b/Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
@@ -482,8 +482,11 @@ def Measurable [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : Prop
 namespace MeasureTheory
 
 set_option quotPrecheck false in
-/-- Notation for `Measurable` with respect to a non-standanrd σ-algebra in the domain. -/
+/-- Notation for `Measurable` with respect to a non-standard σ-algebra in the domain. -/
 scoped notation "Measurable[" m "]" => @Measurable _ _ m _
+/-- Notation for `Measurable` with respect to a non-standard σ-algebra in the domain and codomain.
+-/
+scoped notation "Measurable[" mα ", " mβ "]" => @Measurable _ _ mα mβ
 
 end MeasureTheory
 

diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean b/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
@@ -71,6 +71,9 @@ structure Measure (α : Type*) [MeasurableSpace α] extends OuterMeasure α wher
     toOuterMeasure (⋃ i, f i) = ∑' i, toOuterMeasure (f i)
   trim_le : toOuterMeasure.trim ≤ toOuterMeasure
 
+/-- Notation for `Measure` with respect to a non-standard σ-algebra in the domain. -/
+scoped notation "Measure[" mα "]" α:arg => @Measure α mα
+
 theorem Measure.toOuterMeasure_injective [MeasurableSpace α] :
     Injective (toOuterMeasure : Measure α → OuterMeasure α)
   | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl => rfl

diff --git a/Mathlib/Probability/Kernel/Basic.lean b/Mathlib/Probability/Kernel/Basic.lean
@@ -67,6 +67,14 @@ structure Kernel (α β : Type*) [MeasurableSpace α] [MeasurableSpace β] where
 
 @[deprecated (since := "2024-07-22")] alias kernel := Kernel
 
+/-- Notation for `Kernel` with respect to a non-standard σ-algebra in the domain. -/
+scoped notation "Kernel[" mα "]" α:arg β:arg => @Kernel α β mα _
+
+/-- Notation for `Kernel` with respect to a non-standard σ-algebra in the domain and codomain. -/
+scoped notation "Kernel[" mα ", " mβ "]" α:arg β:arg => @Kernel α β mα mβ
+
+initialize_simps_projections Kernel (toFun → apply)
+
 variable {α β ι : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
 
 namespace Kernel