diff --git a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean index 8ada014a..fabc7ca8 100644 --- a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean +++ b/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 diff --git a/LeanMachineLearning/Online/Bandit/SumRewards.lean b/LeanMachineLearning/Online/Bandit/SumRewards.lean index b59606fd..e9ef8537 100644 --- a/LeanMachineLearning/Online/Bandit/SumRewards.lean +++ b/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 -/ diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean index aafe1dd2..809e7e53 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithm.lean +++ b/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 diff --git a/LeanMachineLearning/SequentialLearning/Deterministic.lean b/LeanMachineLearning/SequentialLearning/Deterministic.lean index d152e58b..0b1b1e1a 100644 --- a/LeanMachineLearning/SequentialLearning/Deterministic.lean +++ b/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 diff --git a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean index 5b2cc49f..e59547b1 100644 --- a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean +++ b/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`. -/ diff --git a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean index 72405acd..4d0736c2 100644 --- a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean +++ b/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 diff --git a/tutorial/Manual/Pages/DefiningAlgorithm.lean b/tutorial/Manual/Pages/DefiningAlgorithm.lean index bf381c01..2e1c752c 100644 --- a/tutorial/Manual/Pages/DefiningAlgorithm.lean +++ b/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