New algorithm and environment classes

LeanMachineLearning.lean

@@ -15,13 +15,16 @@ public import LeanMachineLearning.Probability.Independence.CondIndepFun
 public import LeanMachineLearning.Probability.Independence.IndepFun
 public import LeanMachineLearning.Probability.Independence.IndepInfinitePi
 public import LeanMachineLearning.Probability.Integrable
+public import LeanMachineLearning.Probability.Kernel.Basic
+public import LeanMachineLearning.Probability.Kernel.Composition.MapComap
 public import LeanMachineLearning.Probability.Kernel.IonescuTulcea.Traj
 public import LeanMachineLearning.Probability.Kernel.KernelSub
 public import LeanMachineLearning.Probability.Moments.SubGaussian
 public import LeanMachineLearning.SequentialLearning.Algorithm
 public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling
 public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
 public import LeanMachineLearning.SequentialLearning.Deterministic
+public import LeanMachineLearning.SequentialLearning.EvaluationEnv
 public import LeanMachineLearning.SequentialLearning.FiniteActions
 public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
 public import LeanMachineLearning.SequentialLearning.StationaryEnv

LeanMachineLearning/Probability/Kernel/Basic.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.Probability.Kernel.Basic
+
+@[expose] public section
+
+open MeasureTheory
+
+namespace ProbabilityTheory.Kernel
+
+variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
+
+/-- Two deterministic kernels are equal if and only if their underlying functions are equal. -/
+@[simp]
+lemma deterministic_inj [MeasurableSpace.SeparatesPoints β]
+    {f g : α → β} {hf : Measurable f} {hg : Measurable g} :
+    Kernel.deterministic f hf = Kernel.deterministic g hg ↔ f = g := by
+  simp [Kernel.ext_iff, Kernel.deterministic_apply, dirac_eq_dirac_iff, funext_iff]
+
+end ProbabilityTheory.Kernel

LeanMachineLearning/Probability/Kernel/Composition/MapComap.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.Probability.Kernel.Composition.MapComap
+
+@[expose] public section
+
+namespace ProbabilityTheory.Kernel
+
+variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+
+@[simp]
+lemma prodMkLeft_inj [h_nonempty : Nonempty γ]
+    (κ ν : Kernel α β) :
+    κ.prodMkLeft γ = ν.prodMkLeft γ ↔ κ = ν := by
+  simp only [Kernel.ext_iff, Kernel.prodMkLeft_apply, Prod.forall]
+  exact ⟨fun h b ↦ h h_nonempty.some b, fun h _ b ↦ h b⟩
+
+@[simp]
+lemma prodMkRight_inj [h_nonempty : Nonempty γ]
+    (κ ν : Kernel α β) :
+    κ.prodMkRight γ = ν.prodMkRight γ ↔ κ = ν := by
+  simp only [Kernel.ext_iff, Kernel.prodMkRight_apply, Prod.forall]
+  exact ⟨fun h a ↦ h a h_nonempty.some, fun h a _ ↦ h a⟩
+
+@[simp]
+lemma prodMkLeft_deterministic {f : α → β} (hf : Measurable f) :
+    (Kernel.deterministic f hf).prodMkLeft γ =
+      Kernel.deterministic (fun p ↦ f p.2) (by fun_prop) := by
+  ext
+  simp [Kernel.deterministic_apply]
+
+@[simp]
+lemma prodMkRight_deterministic {f : α → β} (hf : Measurable f) :
+    (Kernel.deterministic f hf).prodMkRight γ =
+      Kernel.deterministic (fun p ↦ f p.1) (by fun_prop) := by
+  ext
+  simp [Kernel.deterministic_apply]
+
+end ProbabilityTheory.Kernel