Cleanup: Ionescu-Tulcea space

LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean

@@ -5,11 +5,11 @@ Authors: Rémy Degenne, Paulo Rauber
 -/
 module
 
+public import LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBorel
 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.MeasureTheory.Constructions.Polish.StandardBorel
 public import LeanMachineLearning.SequentialLearning.FiniteActions
 public import LeanMachineLearning.SequentialLearning.StationaryEnv
 public import Mathlib.Probability.Independence.Integration

LeanMachineLearning/Online/Bandit/SumRewards.lean

@@ -8,6 +8,7 @@ module
 public import LeanMachineLearning.Online.Bandit.ArrayProbSpace
 public import LeanMachineLearning.Online.Bandit.Regret
 public import LeanMachineLearning.Probability.Moments.SubGaussian
+public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
 
 /-! # Law of the sum of rewards
 -/

LeanMachineLearning/SequentialLearning/Algorithm.lean

@@ -25,14 +25,6 @@ interacting with an environment.
 * `IsAlgEnvSeqUntil A R' alg env P N`: `A` and `R'` form an algorithm-environment sequence until
   time `N`.
 
-## Main statements
-
-* `isAlgEnvSeq_unique`: the law of the sequence of actions and observations generated by an
-  algorithm-environment pair is unique: it does not depend on the probability space used.
-  If `A₁`, `R₁` and `A₂`, `R₂` are two algorithm-environment sequences generated by the same
-  algorithm-environment pair on probability spaces `(Ω, P)` and `(Ω', P')`, then
-  `P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω))`.
-
 ## Notes
 
 The `ANCHOR` comments are used to mark code that appears in the tutorials.
@@ -312,61 +304,4 @@ lemma IsAlgEnvSeq.filtrationAction_eq_comap
 
 end IsAlgEnvSeq
 
-/-- Measure on the sequence of actions and observations generated by the algorithm/environment. -/
-noncomputable
-def trajMeasure (alg : Algorithm α R) (env : Environment α R) :
-    Measure (ℕ → α × R) :=
-  Kernel.trajMeasure (alg.p0 ⊗ₘ env.ν0) (stepKernel alg env)
-deriving IsProbabilityMeasure
-
-section ModelEquivalence
-
-variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
-  [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
-  {alg : Algorithm α R} {env : Environment α R}
-  {P : Measure Ω} [IsProbabilityMeasure P] {P' : Measure Ω'} [IsProbabilityMeasure P']
-  {A₁ : ℕ → Ω → α} {R₁ : ℕ → Ω → R} {A₂ : ℕ → Ω' → α} {R₂ : ℕ → Ω' → R} {N : ℕ}
-
-theorem eq_trajMeasure_of_isAlgEnvSeq (h : IsAlgEnvSeq A₁ R₁ alg env P) :
-    P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = trajMeasure alg env := by
-  rw [trajMeasure]
-  have h := Kernel.eq_trajMeasure (Y := fun n ω ↦ (A₁ n ω, R₁ n ω)) (P := P)
-    (μ₀ := alg.p0 ⊗ₘ env.ν0) (κ := stepKernel alg env) (fun n ↦ ?_) ?_ (fun n ↦ ?_)
-  · exact h
-  · have hA := h.measurable_A n
-    have hR := h.measurable_R n
-    fun_prop
-  · simp only
-    exact h.hasLaw_step_zero
-  · exact h.hasCondDistrib_step n
-
-lemma eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil
-    (h : IsAlgEnvSeqUntil A₁ R₁ alg env P N) :
-    P.map (fun ω (n : Iic N) ↦ (A₁ n ω, R₁ n ω)) =
-      (trajMeasure alg env).map (Preorder.frestrictLe N) := by
-  rw [trajMeasure]
-  have h := Kernel.eq_trajMeasure_map_frestrictLe (Y := fun n ω ↦ (A₁ n ω, R₁ n ω))
-    (P := P) (μ₀ := alg.p0 ⊗ₘ env.ν0) (κ := stepKernel alg env) ?_ (fun n hn ↦ ?_) (N := N)
-  · exact h
-  · exact h.hasLaw_step_zero
-  · exact h.hasCondDistrib_step n hn
-
-/-- The law of the sequence of actions and observations generated by an algorithm-environment pair
-is unique: it does not depend on the probability space used. -/
--- ANCHOR: isAlgEnvSeq_unique
-theorem isAlgEnvSeq_unique (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
-    (h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
-    P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω)) := by
--- ANCHOR_END: isAlgEnvSeq_unique
-  rw [eq_trajMeasure_of_isAlgEnvSeq h1, eq_trajMeasure_of_isAlgEnvSeq h2]
-
-theorem isAlgEnvSeqUntil_unique (h1 : IsAlgEnvSeqUntil A₁ R₁ alg env P N)
-    (h2 : IsAlgEnvSeqUntil A₂ R₂ alg env P' N) :
-    P.map (fun ω (n : Iic N) ↦ (A₁ n ω, R₁ n ω)) =
-      P'.map (fun ω (n : Iic N) ↦ (A₂ n ω, R₂ n ω)) := by
-  rw [eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil h1,
-    eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil h2]
-
-end ModelEquivalence
-
 end Learning

LeanMachineLearning/SequentialLearning/Deterministic.lean

@@ -6,7 +6,7 @@ Authors: Rémy Degenne
 module
 
 public import LeanMachineLearning.Probability.Kernel.Basic
-public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
+public import LeanMachineLearning.SequentialLearning.Algorithm
 
 /-!
 # Deterministic algorithms and environments
@@ -308,31 +308,4 @@ lemma action_detAlgorithm_ae_eq
 
 end IsAlgEnvSeqUntil
 
-namespace IT
-
-local notation "𝔓" => trajMeasure (detAlgorithm nextA h_next action0) env
-
-lemma HasLaw_action_zero_detAlgorithm : HasLaw (IT.action 0) (Measure.dirac action0) 𝔓 where
-  map_eq := (IT.hasLaw_action_zero _ _).map_eq
-
-lemma action_zero_detAlgorithm [MeasurableSingletonClass α] :
-    IT.action 0 =ᵐ[𝔓] fun _ ↦ action0 := by
-  have h_eq : ∀ᵐ x ∂((𝔓).map (IT.action 0)), x = action0 := by
-    rw [(IT.hasLaw_action_zero _ _).map_eq]
-    simp [detAlgorithm]
-  exact ae_of_ae_map (by fun_prop) h_eq
-
-lemma action_detAlgorithm_ae_eq [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R]
-    [Nonempty R] (n : ℕ) : IT.action (n + 1) =ᵐ[𝔓] fun h ↦ nextA n (IT.hist n h) :=
-  ae_eq_of_condDistrib_eq_deterministic (by fun_prop) (by fun_prop) (by fun_prop)
-    (IT.condDistrib_action (detAlgorithm nextA h_next action0) env n)
-
-lemma action_detAlgorithm_ae_all_eq
-    [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] :
-    ∀ᵐ h ∂𝔓, IT.action 0 h = action0 ∧ ∀ n, IT.action (n + 1) h = nextA n (IT.hist n h) := by
-  rw [eventually_and, ae_all_iff]
-  exact ⟨action_zero_detAlgorithm, action_detAlgorithm_ae_eq⟩
-
-end IT
-
 end Learning

LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean

@@ -15,7 +15,13 @@ a sequence of random variables representing the actions and feedback generated b
 of the algorithm and the environment.
 The main ingredient of the construction is the Ionescu-Tulcea theorem.
 
-TODO: actually, the probability measure is already defined in the Algorithm file. Reorganize?
+## Main statements
+
+* `isAlgEnvSeq_unique`: the law of the sequence of actions and observations generated by an
+  algorithm-environment pair is unique: it does not depend on the probability space used.
+  If `A₁`, `R₁` and `A₂`, `R₂` are two algorithm-environment sequences generated by the same
+  algorithm-environment pair on probability spaces `(Ω, P)` and `(Ω', P')`, then
+  `P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω))`.
 
 -/
 
@@ -29,6 +35,63 @@ namespace Learning
 
 variable {α R Ω : Type*} {mα : MeasurableSpace α} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω}
 
+/-- Measure on the sequence of actions and observations generated by the algorithm/environment. -/
+noncomputable
+def trajMeasure (alg : Algorithm α R) (env : Environment α R) :
+    Measure (ℕ → α × R) :=
+  Kernel.trajMeasure (alg.p0 ⊗ₘ env.ν0) (stepKernel alg env)
+deriving IsProbabilityMeasure
+
+section ModelEquivalence
+
+variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
+  [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
+  {alg : Algorithm α R} {env : Environment α R}
+  {P : Measure Ω} [IsProbabilityMeasure P] {P' : Measure Ω'} [IsProbabilityMeasure P']
+  {A₁ : ℕ → Ω → α} {R₁ : ℕ → Ω → R} {A₂ : ℕ → Ω' → α} {R₂ : ℕ → Ω' → R} {N : ℕ}
+
+theorem eq_trajMeasure_of_isAlgEnvSeq (h : IsAlgEnvSeq A₁ R₁ alg env P) :
+    P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = trajMeasure alg env := by
+  rw [trajMeasure]
+  have h := Kernel.eq_trajMeasure (Y := fun n ω ↦ (A₁ n ω, R₁ n ω)) (P := P)
+    (μ₀ := alg.p0 ⊗ₘ env.ν0) (κ := stepKernel alg env) (fun n ↦ ?_) ?_ (fun n ↦ ?_)
+  · exact h
+  · have hA := h.measurable_A n
+    have hR := h.measurable_R n
+    fun_prop
+  · simp only
+    exact h.hasLaw_step_zero
+  · exact h.hasCondDistrib_step n
+
+lemma eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil
+    (h : IsAlgEnvSeqUntil A₁ R₁ alg env P N) :
+    P.map (fun ω (n : Iic N) ↦ (A₁ n ω, R₁ n ω)) =
+      (trajMeasure alg env).map (Preorder.frestrictLe N) := by
+  rw [trajMeasure]
+  have h := Kernel.eq_trajMeasure_map_frestrictLe (Y := fun n ω ↦ (A₁ n ω, R₁ n ω))
+    (P := P) (μ₀ := alg.p0 ⊗ₘ env.ν0) (κ := stepKernel alg env) ?_ (fun n hn ↦ ?_) (N := N)
+  · exact h
+  · exact h.hasLaw_step_zero
+  · exact h.hasCondDistrib_step n hn
+
+/-- The law of the sequence of actions and observations generated by an algorithm-environment pair
+is unique: it does not depend on the probability space used. -/
+-- ANCHOR: isAlgEnvSeq_unique
+theorem isAlgEnvSeq_unique (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
+    (h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
+    P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω)) := by
+-- ANCHOR_END: isAlgEnvSeq_unique
+  rw [eq_trajMeasure_of_isAlgEnvSeq h1, eq_trajMeasure_of_isAlgEnvSeq h2]
+
+theorem isAlgEnvSeqUntil_unique (h1 : IsAlgEnvSeqUntil A₁ R₁ alg env P N)
+    (h2 : IsAlgEnvSeqUntil A₂ R₂ alg env P' N) :
+    P.map (fun ω (n : Iic N) ↦ (A₁ n ω, R₁ n ω)) =
+      P'.map (fun ω (n : Iic N) ↦ (A₂ n ω, R₂ n ω)) := by
+  rw [eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil h1,
+    eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil h2]
+
+end ModelEquivalence
+
 namespace IT
 
 /-- Action and reward at step `n`. -/

LeanMachineLearning/SequentialLearning/StationaryEnv.lean

@@ -6,7 +6,7 @@ Authors: Rémy Degenne, Paulo Rauber
 module
 
 public import LeanMachineLearning.Probability.Kernel.Composition.MapComap
-public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
+public import LeanMachineLearning.SequentialLearning.Algorithm
 
 /-!
 # Oblivious and stationary environments
@@ -230,37 +230,4 @@ lemma condIndepFun_reward_hist_action_action' [StandardBorelSpace Ω]
 
 end IsAlgEnvSeq
 
-namespace IT
-
-local notation "𝔓" => trajMeasure alg (stationaryEnv ν)
-
-/-- The conditional distribution of the reward at time `n` given the action at time `n` is `ν`. -/
-lemma condDistrib_reward_stationaryEnv (n : ℕ) :
-    condDistrib (IT.reward n) (IT.action n) 𝔓 =ᵐ[(𝔓).map (IT.action n)] ν :=
-  IsAlgEnvSeq.condDistrib_reward_stationaryEnv
-    (IT.isAlgEnvSeq_trajMeasure alg (stationaryEnv ν)) n
-
-/-- The reward at time `n + 1` is conditionally independent of the history up to time `n`
-given the action at time `n + 1`. -/
-lemma condIndepFun_reward_hist_action (n : ℕ) :
-    IT.reward (n + 1) ⟂ᵢ[IT.action (n + 1), IT.measurable_action _ ; 𝔓] IT.hist n :=
-  IsAlgEnvSeq.condIndepFun_reward_hist_action
-    (IT.isAlgEnvSeq_trajMeasure alg (stationaryEnv ν)) n
-
-lemma condIndepFun_reward_hist_action_action
-    {alg : Algorithm α R} {ν : Kernel α R} [IsMarkovKernel ν] (n : ℕ) :
-    reward (n + 1) ⟂ᵢ[action (n + 1), measurable_action (n + 1); trajMeasure alg (stationaryEnv ν)]
-      (fun ω ↦ (hist n ω, action (n + 1) ω)) :=
-  IsAlgEnvSeq.condIndepFun_reward_hist_action_action
-    (IT.isAlgEnvSeq_trajMeasure alg (stationaryEnv ν)) n
-
-lemma condIndepFun_reward_hist_action_action'
-    {alg : Algorithm α R} {ν : Kernel α R} [IsMarkovKernel ν] (n : ℕ) (hn : n ≠ 0) :
-    reward n ⟂ᵢ[action n, measurable_action n; trajMeasure alg (stationaryEnv ν)]
-      (fun ω ↦ (hist (n - 1) ω, action n ω)) :=
-  IsAlgEnvSeq.condIndepFun_reward_hist_action_action'
-    (IT.isAlgEnvSeq_trajMeasure alg (stationaryEnv ν)) n hn
-
-end IT
-
 end Learning

tutorial/Manual/Pages/DefiningAlgorithm.lean

@@ -115,7 +115,7 @@ All spaces of interest in machine learning are standard Borel, so this is not a
 Given any algorithm and environment, there always exists a sequence of actions and feedback that satisfies `IsAlgEnvSeq` by the Ionescu-Tulcea theorem.
 However other constructions of such sequences are possible, and it is easier to work with generic sequences satisfying `IsAlgEnvSeq` than with a specific construction.
 Which sequence we choose does not matter for the results we prove, since all such sequences are equal in distribution, as stated by the following theorem.
-```anchor isAlgEnvSeq_unique (module := LeanMachineLearning.SequentialLearning.Algorithm)
+```anchor isAlgEnvSeq_unique (module := LeanMachineLearning.SequentialLearning.IonescuTulceaSpace)
 theorem isAlgEnvSeq_unique (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
     (h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
     P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω)) := by