From 515f3a4a3091828c3f4e4539bc6a821daa881679 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 11 Sep 2026 15:50:16 +0200 Subject: [PATCH] experiment: shift filtration --- .../SequentialLearning/ActionIndicator.lean | 16 +-- .../SequentialLearning/Algorithm.lean | 102 ++++++++++-------- .../SequentialLearning/FiniteActions.lean | 54 +++++----- .../IonescuTulceaSpace.lean | 83 +++++++------- .../SequentialLearning/Means.lean | 8 +- .../SequentialLearning/SumRewards.lean | 75 +++++-------- 6 files changed, 173 insertions(+), 165 deletions(-) diff --git a/LeanMachineLearning/SequentialLearning/ActionIndicator.lean b/LeanMachineLearning/SequentialLearning/ActionIndicator.lean index 5b5debc8..9ae78361 100644 --- a/LeanMachineLearning/SequentialLearning/ActionIndicator.lean +++ b/LeanMachineLearning/SequentialLearning/ActionIndicator.lean @@ -24,7 +24,8 @@ at round `n`. It is the increment weight of every per-action sum attached to an * `Learning.sum_range_actionIndicator_eq_pullCount`, `Learning.sum_actionIndicator_mul` β€” the two partial-sum identities. -* `Learning.adapted_actionIndicator`, `Learning.integrable_actionIndicator`. +* `Learning.IsAlgEnvSeq.measurable_actionIndicator_filtration_succ`, + `Learning.integrable_actionIndicator`. -/ @[expose] public section @@ -92,12 +93,13 @@ lemma integrable_actionIndicator (P : Measure Ξ©) [IsFiniteMeasure P] Integrable (actionIndicator A k n) P := (integrable_const (1 : ℝ)).indicator (hA (measurableSet_singleton k)) -/-- The action indicator is adapted to the history filtration: whether action `k` was chosen at `n` -is known at time `n`. -/ -lemma IsAlgEnvSeq.adapted_actionIndicator {alg : Algorithm π“ž 𝓐 𝓨} {env : Environment π“ž 𝓐 𝓨} - [IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (k : 𝓐) : - Adapted h.filtration (actionIndicator A k) := - fun _ ↦ Measurable.indicator measurable_const (h.adapted_action _ (measurableSet_singleton k)) +/-- Whether action `k` was chosen at time `n` is known once the first `n + 1` rounds are known. -/ +lemma IsAlgEnvSeq.measurable_actionIndicator_filtration_succ {alg : Algorithm π“ž 𝓐 𝓨} + {env : Environment π“ž 𝓐 𝓨} [IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (k : 𝓐) + (n : β„•) : + Measurable[h.filtration (n + 1)] (actionIndicator A k n) := + Measurable.indicator measurable_const + (h.measurable_action_filtration_succ n (measurableSet_singleton k)) /-- The action indicator is adapted to the history+action filtration: whether action `k` was chosen at `n` is known once we know the action at `n`. -/ diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean index bfd28276..a765d142 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithm.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean @@ -539,56 +539,75 @@ section Filtration namespace IsAlgEnvSeq -/-- Filtration generated by the history up to time `n` (included): `h.filtration n` is the -Οƒ-algebra generated by `history O A Y (n + 1)`, that is by the rounds at times `0, ..., n`. -/ +/-- Filtration generated by the history: `h.filtration n` is the Οƒ-algebra generated by +`history O A Y n`, that is by the `n` rounds at times `0, ..., n - 1`. In particular +`h.filtration 0` is the trivial Οƒ-algebra, and the round at time `n` is measurable with respect +to `h.filtration (n + 1)`. -/ def filtration (h : IsAlgEnvSeq O A Y alg env P) : Filtration β„• mΞ© where - seq n := MeasurableSpace.comap (history O A Y (n + 1)) inferInstance + seq n := MeasurableSpace.comap (history O A Y n) inferInstance mono' i j hij := by simp only - rw [← measurable_iff_comap_le, history_eq_comp_history (Nat.succ_le_succ hij)] + rw [← measurable_iff_comap_le, history_eq_comp_history hij] exact measurable_comp_comap _ (by fun_prop) le' i := by rw [← measurable_iff_comap_le] exact Learning.measurable_history h.measurable_obs h.measurable_action h.measurable_feedback _ lemma filtration_eq_comap (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : - h.filtration n = MeasurableSpace.comap (history O A Y (n + 1)) inferInstance := rfl + h.filtration n = MeasurableSpace.comap (history O A Y n) inferInstance := rfl -lemma measurable_history_succ_filtration (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : - Measurable[h.filtration n] (history O A Y (n + 1)) := +lemma filtration_zero (h : IsAlgEnvSeq O A Y alg env P) : h.filtration 0 = βŠ₯ := by + rw [filtration_eq_comap, history_zero, MeasurableSpace.comap_const] + +lemma measurable_history_filtration (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : + Measurable[h.filtration n] (history O A Y n) := measurable_iff_comap_le.mpr le_rfl lemma adapted_history (h : IsAlgEnvSeq O A Y alg env P) : - Adapted h.filtration (history O A Y) := by - intro n - rw [history_eq_comp_history n.le_succ] - exact measurable_comp_comap _ (by fun_prop) + Adapted h.filtration (history O A Y) := + h.measurable_history_filtration -lemma adapted_step (h : IsAlgEnvSeq O A Y alg env P) : - Adapted h.filtration (step O A Y) := by - intro n +lemma measurable_step_filtration_succ (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : + Measurable[h.filtration (n + 1)] (step O A Y n) := by rw [← eval_comp_history] exact measurable_comp_comap _ (by fun_prop) -lemma adapted_obs (h : IsAlgEnvSeq O A Y alg env P) : - Adapted h.filtration O := by - intro n +lemma measurable_obs_filtration_succ (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : + Measurable[h.filtration (n + 1)] (O n) := by rw [← obs_eval_comp_history (O := O) (A := A) (Y := Y) n] exact measurable_comp_comap _ (by fun_prop) -lemma adapted_action (h : IsAlgEnvSeq O A Y alg env P) : - Adapted h.filtration A := by - intro n +lemma measurable_action_filtration_succ (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : + Measurable[h.filtration (n + 1)] (A n) := by rw [← action_eval_comp_history (O := O) (A := A) (Y := Y) n] exact measurable_comp_comap _ (by fun_prop) -lemma adapted_feedback (h : IsAlgEnvSeq O A Y alg env P) : - Adapted h.filtration Y := by - intro n +lemma measurable_feedback_filtration_succ (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : + Measurable[h.filtration (n + 1)] (Y n) := by rw [← feedback_eval_comp_history (O := O) (A := A) (Y := Y) n] exact measurable_comp_comap _ (by fun_prop) +/-- The step at time `m < n` is measurable with respect to the Οƒ-algebra generated by the first +`n` rounds. -/ +lemma measurable_step_filtration_of_lt (h : IsAlgEnvSeq O A Y alg env P) {m n : β„•} (hmn : m < n) : + Measurable[h.filtration n] (step O A Y m) := + (h.measurable_step_filtration_succ m).mono (h.filtration.mono hmn) le_rfl + +lemma measurable_obs_filtration_of_lt (h : IsAlgEnvSeq O A Y alg env P) {m n : β„•} (hmn : m < n) : + Measurable[h.filtration n] (O m) := + (h.measurable_obs_filtration_succ m).mono (h.filtration.mono hmn) le_rfl + +lemma measurable_action_filtration_of_lt (h : IsAlgEnvSeq O A Y alg env P) {m n : β„•} + (hmn : m < n) : + Measurable[h.filtration n] (A m) := + (h.measurable_action_filtration_succ m).mono (h.filtration.mono hmn) le_rfl + +lemma measurable_feedback_filtration_of_lt (h : IsAlgEnvSeq O A Y alg env P) {m n : β„•} + (hmn : m < n) : + Measurable[h.filtration n] (Y m) := + (h.measurable_feedback_filtration_succ m).mono (h.filtration.mono hmn) le_rfl + /-- Filtration generated by the history before time `n` together with the observation at time `n`. -/ def filtrationObs (h : IsAlgEnvSeq O A Y alg env P) : @@ -677,22 +696,23 @@ lemma filtrationObs_le_filtrationAction (h : IsAlgEnvSeq O A Y alg env P) (n : rw [filtrationObs_eq_comap, filtrationAction_eq_comap, ← measurable_iff_comap_le] exact measurable_fst.comp (measurable_iff_comap_le.mpr le_rfl) -lemma filtration_le_filtrationObs_succ (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : - h.filtration n ≀ h.filtrationObs (n + 1) := - measurable_iff_comap_le.mp (h.measurable_history_filtrationObs (n + 1)) +lemma filtration_le_filtrationObs (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : + h.filtration n ≀ h.filtrationObs n := + measurable_iff_comap_le.mp (h.measurable_history_filtrationObs n) -lemma filtration_le_filtrationAction_succ (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : - h.filtration n ≀ h.filtrationAction (n + 1) := - measurable_iff_comap_le.mp (h.measurable_history_filtrationAction (n + 1)) +lemma filtration_le_filtrationAction (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : + h.filtration n ≀ h.filtrationAction n := + measurable_iff_comap_le.mp (h.measurable_history_filtrationAction n) -lemma filtrationAction_le_filtration (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : - h.filtrationAction n ≀ h.filtration n := by +lemma filtrationAction_le_filtration_succ (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : + h.filtrationAction n ≀ h.filtration (n + 1) := by rw [filtrationAction_eq_comap, ← measurable_iff_comap_le] - exact ((h.adapted_history n).prodMk (h.adapted_obs n)).prodMk (h.adapted_action n) + exact ((h.adapted_history.measurable_le n.le_succ).prodMk + (h.measurable_obs_filtration_succ n)).prodMk (h.measurable_action_filtration_succ n) -lemma filtrationObs_le_filtration (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : - h.filtrationObs n ≀ h.filtration n := - (h.filtrationObs_le_filtrationAction n).trans (h.filtrationAction_le_filtration n) +lemma filtrationObs_le_filtration_succ (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : + h.filtrationObs n ≀ h.filtration (n + 1) := + (h.filtrationObs_le_filtrationAction n).trans (h.filtrationAction_le_filtration_succ n) lemma adapted_obs_filtrationObs (h : IsAlgEnvSeq O A Y alg env P) : Adapted h.filtrationObs O := fun _ ↦ @@ -708,17 +728,13 @@ lemma adapted_action_filtrationAction (h : IsAlgEnvSeq O A Y alg env P) : lemma measurable_feedback_filtrationObs_of_lt (h : IsAlgEnvSeq O A Y alg env P) {m n : β„•} (hmn : m < n) : - Measurable[h.filtrationObs n] (Y m) := by - obtain ⟨j, rfl⟩ : βˆƒ j, n = j + 1 := ⟨n - 1, by lia⟩ - exact (h.adapted_feedback.measurable_le (by lia)).mono - (filtration_le_filtrationObs_succ h j) le_rfl + Measurable[h.filtrationObs n] (Y m) := + (h.measurable_feedback_filtration_of_lt hmn).mono (filtration_le_filtrationObs h n) le_rfl lemma measurable_feedback_filtrationAction_of_lt (h : IsAlgEnvSeq O A Y alg env P) {m n : β„•} (hmn : m < n) : - Measurable[h.filtrationAction n] (Y m) := by - obtain ⟨j, rfl⟩ : βˆƒ j, n = j + 1 := ⟨n - 1, by lia⟩ - exact (h.adapted_feedback.measurable_le (by lia)).mono - (filtration_le_filtrationAction_succ h j) le_rfl + Measurable[h.filtrationAction n] (Y m) := + (h.measurable_feedback_filtration_of_lt hmn).mono (filtration_le_filtrationAction h n) le_rfl end IsAlgEnvSeq diff --git a/LeanMachineLearning/SequentialLearning/FiniteActions.lean b/LeanMachineLearning/SequentialLearning/FiniteActions.lean index b0ca865b..9138b5ef 100644 --- a/LeanMachineLearning/SequentialLearning/FiniteActions.lean +++ b/LeanMachineLearning/SequentialLearning/FiniteActions.lean @@ -219,27 +219,20 @@ lemma measurable_uncurry_pullCount' [MeasurableEq 𝓐] (n : β„•) : exact measurableSet_eq_fun (by fun_prop) (by fun_prop) fun_prop -lemma adapted_pullCount_add_one [MeasurableSingletonClass 𝓐] +/-- The number of pulls of `a` before time `n` is a function of the first `n` rounds. -/ +lemma adapted_pullCount [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) : - Adapted h.filtration (fun n ↦ pullCount A a (n + 1)) := by + Adapted h.filtration (pullCount A a) := by intro n - change Measurable[h.filtration n] (pullCount A a (n + 1)) + change Measurable[h.filtration n] (pullCount A a n) rw [measurable_iff_comap_le, h.filtration_eq_comap, pullCount_eq_comp_history (O := O) (R' := R'), ← measurable_iff_comap_le] - exact measurable_comp_comap _ (measurable_pullCount' (n + 1) a) + exact measurable_comp_comap _ (measurable_pullCount' n a) -lemma stronglyAdapted_pullCount_add_one [MeasurableSingletonClass 𝓐] +lemma stronglyAdapted_pullCount [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) : - StronglyAdapted h.filtration (fun n ↦ pullCount A a (n + 1)) := - (adapted_pullCount_add_one h a).stronglyAdapted - -lemma isStronglyPredictable_pullCount [MeasurableSingletonClass 𝓐] - (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) : - IsStronglyPredictable h.filtration (pullCount A a) := by - rw [IsStronglyPredictable.iff_measurable_add_one] - refine ⟨?_, stronglyAdapted_pullCount_add_one h a⟩ - simp only [pullCount_zero] - fun_prop + StronglyAdapted h.filtration (pullCount A a) := + (adapted_pullCount h a).stronglyAdapted lemma measurableSet_action_eq_and_pullCount_eq [MeasurableSingletonClass 𝓐] (hA : βˆ€ n, Measurable (A n)) (t : β„•) (b : 𝓐) (k : β„•) : @@ -529,16 +522,6 @@ lemma stepsUntil_eq_congr {Ο‰' : Ξ©} (h_eq : βˆ€ i ≀ n, A i Ο‰ = A i Ο‰') : section Measurability -lemma isStoppingTime_stepsUntil [MeasurableSingletonClass 𝓐] - (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) (hm : m β‰  0) : - IsStoppingTime h.filtration (stepsUntil A a m) := by - rw [stepsUntil_eq_leastGE _ hm] - refine StronglyAdapted.isStoppingTime_leastGE _ fun n ↦ ?_ - suffices StronglyMeasurable[h.filtration n] (pullCount A a (n + 1)) by - fun_prop - refine Measurable.stronglyMeasurable ?_ - exact adapted_pullCount_add_one h a n - -- todo: get this from the stopping time property? @[fun_prop] lemma measurable_stepsUntil [MeasurableSingletonClass 𝓐] @@ -644,6 +627,27 @@ lemma isStoppingTime_stepsUntil_filtrationAction [MeasurableSingletonClass 𝓐] rw [h.filtrationAction_eq_comap n] exact measurableSet_stepsUntil_eq O R' a m n +/-- `stepsUntil a m + 1`, the number of rounds played until action `a` has been pulled `m` +times, is a stopping time with respect to the history filtration (`stepsUntil a m` itself is the +index of the round of the `m`-th pull, which is known only once that round is played). -/ +lemma isStoppingTime_stepsUntil_add_one [MeasurableSingletonClass 𝓐] + (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) (m : β„•) : + IsStoppingTime h.filtration (fun Ο‰ ↦ (stepsUntil A a m Ο‰ + 1 : β„•βˆž)) := by + intro n + change MeasurableSet[h.filtration n] {Ο‰ | stepsUntil A a m Ο‰ + 1 ≀ (n : β„•βˆž)} + cases n with + | zero => + convert @MeasurableSet.empty Ξ© (h.filtration 0) using 1 + ext Ο‰ + simp only [Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false] + exact fun h' ↦ absurd (le_add_self.trans h') (by simp) + | succ j => + convert h.filtrationAction_le_filtration_succ j _ + (isStoppingTime_stepsUntil_filtrationAction h a m j) using 1 + ext Ο‰ + simp only [Set.mem_ofPred_eq, ENat.some_eq_natCast, Nat.cast_add, Nat.cast_one] + exact ENat.add_le_add_iff_right (by simp) + end Measurability end StepsUntil diff --git a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean index 515c6874..1548b95c 100644 --- a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean +++ b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean @@ -189,49 +189,55 @@ end ModelEquivalence namespace IT -/-- Filtration of the algorithm Seq: `IT.filtration π“ž 𝓐 𝓨 n` is the Οƒ-algebra generated by the -rounds at times `0, ..., n`, that is by `hist (n + 1)`. -/ +/-- Filtration of the canonical space: `IT.filtration π“ž 𝓐 𝓨 n` is the Οƒ-algebra generated by +`hist n`, that is by the `n` rounds at times `0, ..., n - 1`. -/ protected def filtration (π“ž 𝓐 𝓨 : Type*) [MeasurableSpace π“ž] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] : - Filtration β„• (inferInstance : MeasurableSpace (β„• β†’ Round π“ž 𝓐 𝓨)) := - MeasureTheory.Filtration.piLE (X := fun _ ↦ Round π“ž 𝓐 𝓨) + Filtration β„• (inferInstance : MeasurableSpace (β„• β†’ Round π“ž 𝓐 𝓨)) where + seq n := MeasurableSpace.comap (hist n) inferInstance + mono' i j hij := by + simp only + rw [← measurable_iff_comap_le, hist_eq_comp_hist hij] + exact measurable_comp_comap _ (by fun_prop) + le' n := (measurable_hist n).comap_le lemma filtration_eq_comap (n : β„•) : - IT.filtration π“ž 𝓐 𝓨 n = MeasurableSpace.comap (hist (n + 1)) inferInstance := by - simp only [IT.filtration, Filtration.piLE_eq_comap_frestrictLe] + IT.filtration π“ž 𝓐 𝓨 n = MeasurableSpace.comap (hist n) inferInstance := rfl + +/-- `IT.filtration π“ž 𝓐 𝓨 (n + 1)` is the canonical filtration `Filtration.piLE` of the product +space at time `n`, the Οƒ-algebra generated by the coordinates `0, ..., n`. -/ +lemma filtration_succ_eq_piLE (n : β„•) : + IT.filtration π“ž 𝓐 𝓨 (n + 1) = Filtration.piLE (X := fun _ ↦ Round π“ž 𝓐 𝓨) n := by + rw [filtration_eq_comap, Filtration.piLE_eq_comap_frestrictLe] refine le_antisymm ?_ ?_ - Β· rw [← measurable_iff_comap_le, frestrictLe_eq_comp_hist] - exact measurable_comp_comap _ (by fun_prop) Β· rw [← measurable_iff_comap_le, hist_succ_eq_comp_frestrictLe] exact measurable_comp_comap _ (by fun_prop) + Β· rw [← measurable_iff_comap_le, frestrictLe_eq_comp_hist] + exact measurable_comp_comap _ (by fun_prop) + +lemma measurable_hist_filtration (n : β„•) : + Measurable[IT.filtration π“ž 𝓐 𝓨 n] (hist (π“ž := π“ž) (𝓐 := 𝓐) (𝓨 := 𝓨) n) := + measurable_iff_comap_le.mpr le_rfl + +lemma adapted_hist : Adapted (IT.filtration π“ž 𝓐 𝓨) hist := measurable_hist_filtration -lemma adapted_step : Adapted (IT.filtration π“ž 𝓐 𝓨) (step (π“ž := π“ž) (𝓐 := 𝓐) (𝓨 := 𝓨)) := by - intro n +lemma measurable_step_filtration_succ (n : β„•) : + Measurable[IT.filtration π“ž 𝓐 𝓨 (n + 1)] (step (π“ž := π“ž) (𝓐 := 𝓐) (𝓨 := 𝓨) n) := by rw [filtration_eq_comap, step_eq_eval_comp_hist] exact measurable_comp_comap _ (by fun_prop) -lemma adapted_obs : Adapted (IT.filtration π“ž 𝓐 𝓨) obs := by - intro n +lemma measurable_obs_filtration_succ (n : β„•) : + Measurable[IT.filtration π“ž 𝓐 𝓨 (n + 1)] (obs (π“ž := π“ž) (𝓐 := 𝓐) (𝓨 := 𝓨) n) := by rw [filtration_eq_comap, obs_eq_eval_comp_hist] exact measurable_comp_comap _ (by fun_prop) -lemma measurable_hist_succ_filtration (n : β„•) : - Measurable[IT.filtration π“ž 𝓐 𝓨 n] (hist (n + 1)) := by - rw [filtration_eq_comap] - exact measurable_iff_comap_le.mpr le_rfl - -lemma adapted_hist : Adapted (IT.filtration π“ž 𝓐 𝓨) hist := by - intro n - rw [filtration_eq_comap, hist_eq_comp_hist n.le_succ] - exact measurable_comp_comap _ (by fun_prop) - -lemma adapted_action : Adapted (IT.filtration π“ž 𝓐 𝓨) action := by - intro n +lemma measurable_action_filtration_succ (n : β„•) : + Measurable[IT.filtration π“ž 𝓐 𝓨 (n + 1)] (action (π“ž := π“ž) (𝓐 := 𝓐) (𝓨 := 𝓨) n) := by rw [filtration_eq_comap, action_eq_eval_comp_hist] exact measurable_comp_comap _ (by fun_prop) -lemma adapted_feedback : Adapted (IT.filtration π“ž 𝓐 𝓨) feedback := by - intro n +lemma measurable_feedback_filtration_succ (n : β„•) : + Measurable[IT.filtration π“ž 𝓐 𝓨 (n + 1)] (feedback (π“ž := π“ž) (𝓐 := 𝓐) (𝓨 := 𝓨) n) := by rw [filtration_eq_comap, feedback_eq_eval_comp_hist] exact measurable_comp_comap _ (by fun_prop) @@ -281,24 +287,23 @@ lemma measurable_hist_filtrationAction (n : β„•) : Measurable[filtrationAction π“ž 𝓐 𝓨 n] (hist n) := (measurable_fst.comp measurable_fst).comp (measurable_iff_comap_le.mpr le_rfl) -lemma filtration_le_filtrationAction_add_one (n : β„•) : - IT.filtration π“ž 𝓐 𝓨 n ≀ filtrationAction π“ž 𝓐 𝓨 (n + 1) := by - rw [filtration_eq_comap] - exact measurable_iff_comap_le.mp (measurable_hist_filtrationAction (n + 1)) +lemma filtration_le_filtrationAction (n : β„•) : + IT.filtration π“ž 𝓐 𝓨 n ≀ filtrationAction π“ž 𝓐 𝓨 n := + measurable_iff_comap_le.mp (measurable_hist_filtrationAction n) -lemma filtration_le_filtrationAction {m n : β„•} (h : n < m) : - IT.filtration π“ž 𝓐 𝓨 n ≀ filtrationAction π“ž 𝓐 𝓨 m := by - have h' : n + 1 ≀ m := by grind - exact (filtration_le_filtrationAction_add_one n).trans ((filtrationAction π“ž 𝓐 𝓨).mono h') +lemma filtration_le_filtrationAction_of_le {m n : β„•} (h : n ≀ m) : + IT.filtration π“ž 𝓐 𝓨 n ≀ filtrationAction π“ž 𝓐 𝓨 m := + (filtration_le_filtrationAction n).trans ((filtrationAction π“ž 𝓐 𝓨).mono h) -lemma filtrationAction_le_filtration_self (n : β„•) : - filtrationAction π“ž 𝓐 𝓨 n ≀ IT.filtration π“ž 𝓐 𝓨 n := by +lemma filtrationAction_le_filtration_succ (n : β„•) : + filtrationAction π“ž 𝓐 𝓨 n ≀ IT.filtration π“ž 𝓐 𝓨 (n + 1) := by rw [filtrationAction_eq_comap, ← measurable_iff_comap_le] - exact ((adapted_hist n).prodMk (adapted_obs n)).prodMk (adapted_action n) + exact ((Adapted.measurable_le adapted_hist n.le_succ).prodMk + (measurable_obs_filtration_succ n)).prodMk (measurable_action_filtration_succ n) -lemma filtrationAction_le_filtration {m n : β„•} (h : m ≀ n) : +lemma filtrationAction_le_filtration_of_lt {m n : β„•} (h : m < n) : filtrationAction π“ž 𝓐 𝓨 m ≀ IT.filtration π“ž 𝓐 𝓨 n := - (filtrationAction_le_filtration_self m).trans ((IT.filtration π“ž 𝓐 𝓨).mono h) + (filtrationAction_le_filtration_succ m).trans ((IT.filtration π“ž 𝓐 𝓨).mono h) lemma measurable_obs_filtrationAction (n : β„•) : Measurable[filtrationAction π“ž 𝓐 𝓨 n] (obs n) := diff --git a/LeanMachineLearning/SequentialLearning/Means.lean b/LeanMachineLearning/SequentialLearning/Means.lean index 6207a34f..c2f32147 100644 --- a/LeanMachineLearning/SequentialLearning/Means.lean +++ b/LeanMachineLearning/SequentialLearning/Means.lean @@ -116,10 +116,10 @@ lemma IsAlgEnvSeq.stronglyAdapted_means_filtrationAction [SecondCountableTopolog StronglyAdapted h.filtrationAction (fun n Ο‰ ↦ env.means O A Y (A n Ο‰) n Ο‰) := (h.adapted_means_filtrationAction).stronglyAdapted -lemma IsAlgEnvSeq.adapted_means [SecondCountableTopology 𝓨] [BorelSpace 𝓨] - (h : IsAlgEnvSeq O A Y alg env P) : - Adapted h.filtration (fun n Ο‰ ↦ env.means O A Y (A n Ο‰) n Ο‰) := - fun n ↦ (h.adapted_means_filtrationAction n).mono (h.filtrationAction_le_filtration n) le_rfl +lemma IsAlgEnvSeq.measurable_means_filtration_succ [SecondCountableTopology 𝓨] [BorelSpace 𝓨] + (h : IsAlgEnvSeq O A Y alg env P) (n : β„•) : + Measurable[h.filtration (n + 1)] (fun Ο‰ ↦ env.means O A Y (A n Ο‰) n Ο‰) := + (h.adapted_means_filtrationAction n).mono (h.filtrationAction_le_filtration_succ n) le_rfl omit [NormedSpace ℝ 𝓨] in lemma IsAlgEnvSeq.condExp_feedback_comp {𝓩 : Type*} [NormedAddCommGroup 𝓩] [NormedSpace ℝ 𝓩] diff --git a/LeanMachineLearning/SequentialLearning/SumRewards.lean b/LeanMachineLearning/SequentialLearning/SumRewards.lean index 820cd4ef..3a0d1f2e 100644 --- a/LeanMachineLearning/SequentialLearning/SumRewards.lean +++ b/LeanMachineLearning/SequentialLearning/SumRewards.lean @@ -187,64 +187,45 @@ lemma measurable_uncurry_empMean' [MeasurableEq 𝓐] (n : β„•) : variable [MeasurableSingletonClass 𝓐] -lemma IsAlgEnvSeq.isStronglyPredictable_sumRewards {𝓨 : Type*} {_ : MeasurableSpace 𝓨} +/-- The sum of rewards of action `a` before time `n` is a function of the first `n` rounds. -/ +lemma IsAlgEnvSeq.adapted_sumRewards [MeasurableAddβ‚‚ 𝓨] + {alg : Algorithm π“ž 𝓐 𝓨} {env : Environment π“ž 𝓐 𝓨} + (h : IsAlgEnvSeq O A R alg env P) (a : 𝓐) : + Adapted h.filtration (sumRewards A R a) := by + intro n + change Measurable[h.filtration n] (sumRewards A R a n) + rw [measurable_iff_comap_le, h.filtration_eq_comap, sumRewards_eq_comp_history (O := O), + ← measurable_iff_comap_le] + exact measurable_comp_comap _ (measurable_sumRewards' n a) + +lemma IsAlgEnvSeq.stronglyAdapted_sumRewards {𝓨 : Type*} {_ : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [OpensMeasurableSpace 𝓨] [SecondCountableTopology 𝓨] {R : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm π“ž 𝓐 𝓨} {env : Environment π“ž 𝓐 𝓨} (h : IsAlgEnvSeq O A R alg env P) (a : 𝓐) : - IsStronglyPredictable h.filtration (sumRewards A R a) := by - rw [IsStronglyPredictable.iff_measurable_add_one] - constructor - Β· simp only [sumRewards_zero] - fun_prop + StronglyAdapted h.filtration (sumRewards A R a) := by refine fun n ↦ Finset.stronglyMeasurable_fun_sum _ fun i hi ↦ (Measurable.ite ?_ ?_ (by fun_prop)).stronglyMeasurable Β· refine (measurableSet_singleton a).preimage ?_ - have h_meas_i := h.adapted_action i - simp only [mem_range] at hi - exact h_meas_i.mono (h.filtration.mono (by lia)) le_rfl - Β· have h_meas_i := h.adapted_feedback i simp only [mem_range] at hi - exact h_meas_i.mono (h.filtration.mono (by lia)) le_rfl - -lemma IsAlgEnvSeq.stronglyAdapted_sumRewards_add_one {𝓨 : Type*} {_ : MeasurableSpace 𝓨} - [NormedAddCommGroup 𝓨] [OpensMeasurableSpace 𝓨] [SecondCountableTopology 𝓨] - {R : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm π“ž 𝓐 𝓨} {env : Environment π“ž 𝓐 𝓨} - (h : IsAlgEnvSeq O A R alg env P) (a : 𝓐) : - StronglyAdapted h.filtration (fun n ↦ sumRewards A R a (n + 1)) := by - have h_predictable := h.isStronglyPredictable_sumRewards a - rw [IsStronglyPredictable.iff_measurable_add_one] at h_predictable - exact h_predictable.2 - --- TODO: give a direct proof, without a topology -lemma IsAlgEnvSeq.adapted_sumRewards_add_one {𝓨 : Type*} {_ : MeasurableSpace 𝓨} - [NormedAddCommGroup 𝓨] [BorelSpace 𝓨] [SecondCountableTopology 𝓨] - {R : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm π“ž 𝓐 𝓨} {env : Environment π“ž 𝓐 𝓨} - (h : IsAlgEnvSeq O A R alg env P) (a : 𝓐) : - Adapted h.filtration (fun n ↦ sumRewards A R a (n + 1)) := - (h.stronglyAdapted_sumRewards_add_one a).adapted + exact h.measurable_action_filtration_of_lt hi + Β· simp only [mem_range] at hi + exact h.measurable_feedback_filtration_of_lt hi -lemma IsAlgEnvSeq.isStronglyPredictable_empMean {R' : β„• β†’ Ξ© β†’ ℝ} +/-- The empirical mean of action `a` before time `n` is a function of the first `n` rounds. -/ +lemma IsAlgEnvSeq.adapted_empMean {R' : β„• β†’ Ξ© β†’ ℝ} {alg : Algorithm π“ž 𝓐 ℝ} {env : Environment π“ž 𝓐 ℝ} (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) : - IsStronglyPredictable h.filtration (empMean A R' a) := by - unfold empMean - refine StronglyMeasurable.div ?_ ?_ - Β· exact h.isStronglyPredictable_sumRewards a - Β· have h_meas := (isStronglyPredictable_pullCount h a).measurable - fun_prop - -lemma IsAlgEnvSeq.stronglyAdapted_empMean_add_one - {R' : β„• β†’ Ξ© β†’ ℝ} {alg : Algorithm π“ž 𝓐 ℝ} {env : Environment π“ž 𝓐 ℝ} - (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) : - StronglyAdapted h.filtration (fun n ↦ empMean A R' a (n + 1)) := by - have h_predictable := h.isStronglyPredictable_empMean a - rw [IsStronglyPredictable.iff_measurable_add_one] at h_predictable - exact h_predictable.2 - -lemma IsAlgEnvSeq.adapted_empMean_add_one {R' : β„• β†’ Ξ© β†’ ℝ} + Adapted h.filtration (empMean A R' a) := by + intro n + change Measurable[h.filtration n] (empMean A R' a n) + rw [measurable_iff_comap_le, h.filtration_eq_comap, empMean_eq_comp_history (O := O), + ← measurable_iff_comap_le] + exact measurable_comp_comap _ (measurable_empMean' n a) + +lemma IsAlgEnvSeq.stronglyAdapted_empMean {R' : β„• β†’ Ξ© β†’ ℝ} {alg : Algorithm π“ž 𝓐 ℝ} {env : Environment π“ž 𝓐 ℝ} (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) : - Adapted h.filtration (fun n ↦ empMean A R' a (n + 1)) := - (h.stronglyAdapted_empMean_add_one a).adapted + StronglyAdapted h.filtration (empMean A R' a) := + (h.adapted_empMean a).stronglyAdapted end Learning