Update Mathlib

LeanBandits.lean

@@ -5,8 +5,6 @@ import LeanBandits.Bandit
 import LeanBandits.ETC
 import LeanBandits.ForMathlib.CondDistrib
 import LeanBandits.ForMathlib.IdentDistrib
-import LeanBandits.ForMathlib.KernelCompositionLemmas
-import LeanBandits.ForMathlib.KernelCompositionParallelComp
 import LeanBandits.ForMathlib.KernelSub
 import LeanBandits.ForMathlib.Measurable
 import LeanBandits.ForMathlib.SubGaussian

LeanBandits/Algorithm.lean

@@ -5,7 +5,6 @@ Authors: Rémy Degenne, Paulo Rauber
 -/
 import Mathlib
 import LeanBandits.ForMathlib.CondDistrib
-import LeanBandits.ForMathlib.KernelCompositionLemmas
 import LeanBandits.ForMathlib.Measurable
 import LeanBandits.ForMathlib.Traj
 
@@ -132,6 +131,54 @@ protected def filtration (α R : Type*) [MeasurableSpace α] [MeasurableSpace R]
     Filtration ℕ (inferInstance : MeasurableSpace (ℕ → α × R)) :=
   MeasureTheory.Filtration.piLE (X := fun _ ↦ α × R)
 
+lemma step_eq_eval_comp_hist (n : ℕ) :
+    step (α := α) (R := R) n = (fun x ↦ x ⟨n, by simp⟩) ∘ (hist n) := rfl
+
+lemma action_eq_eval_comp_hist (n : ℕ) :
+    action (α := α) (R := R) n = (fun x ↦ (x ⟨n, by simp⟩).1) ∘ (hist n) := rfl
+
+lemma reward_eq_eval_comp_hist (n : ℕ) :
+    reward (α := α) (R := R) n = (fun x ↦ (x ⟨n, by simp⟩).2) ∘ (hist n) := rfl
+
+lemma measurable_step_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (step n) := by
+  simp only [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe]
+  rw [step_eq_eval_comp_hist]
+  exact measurable_comp_comap _ (by fun_prop)
+
+lemma adapted_step [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
+    [SecondCountableTopology α] [OpensMeasurableSpace α]
+    [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R]
+    [SecondCountableTopology R] [OpensMeasurableSpace R] :
+    Adapted (Learning.filtration α R) (fun n ↦ step (α := α) (R := R) n) :=
+  fun n ↦ (measurable_step_filtration n).stronglyMeasurable
+
+lemma measurable_hist_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (hist n) := by
+  simp [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe,
+    measurable_iff_comap_le]
+
+-- todo: due to the type of `Adapted` and the fact that `Iic n → α × R` depends on `n`, we cannot
+-- state that `hist` is adapted.
+
+lemma measurable_action_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (action n) := by
+  simp only [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe]
+  rw [action_eq_eval_comp_hist]
+  exact measurable_comp_comap _ (by fun_prop)
+
+lemma adapted_action [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
+    [SecondCountableTopology α] [OpensMeasurableSpace α] :
+    Adapted (Learning.filtration α R) action :=
+  fun n ↦ (measurable_action_filtration n).stronglyMeasurable
+
+lemma measurable_reward_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (reward n) := by
+  simp only [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe]
+  rw [reward_eq_eval_comp_hist]
+  exact measurable_comp_comap _ (by fun_prop)
+
+lemma adapted_reward [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R]
+    [SecondCountableTopology R] [OpensMeasurableSpace R] :
+    Adapted (Learning.filtration α R) reward :=
+  fun n ↦ (measurable_reward_filtration n).stronglyMeasurable
+
 lemma condDistrib_step [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
     (alg : Algorithm α R) (env : Environment α R) (n : ℕ) :
     condDistrib (step (n + 1)) (hist n) (trajMeasure alg env)
@@ -143,7 +190,7 @@ lemma condDistrib_action [StandardBorelSpace α] [Nonempty α] [StandardBorelSpa
     condDistrib (action (n + 1)) (hist n) (trajMeasure alg env)
       =ᵐ[(trajMeasure alg env).map (hist n)] alg.policy n := by
   rw [← fst_comp_step]
-  refine (condDistrib_comp' (by fun_prop) (by fun_prop) (by fun_prop)).trans ?_
+  refine (condDistrib_comp _ (by fun_prop) (by fun_prop)).trans ?_
   filter_upwards [condDistrib_step alg env n] with h h_eq
   rw [Kernel.map_apply _ (by fun_prop), h_eq, ← Kernel.map_apply _ (by fun_prop), ← Kernel.fst_eq,
     fst_stepKernel]
@@ -154,8 +201,8 @@ lemma condDistrib_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpa
       =ᵐ[(trajMeasure alg env).map (fun ω ↦ (hist n ω, action (n + 1) ω))] env.feedback n := by
   have h_step := condDistrib_step alg env n
   have h_action := condDistrib_action alg env n
-  rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)] at h_step h_action ⊢
-  rw [h_action, Measure.compProd_assoc, ← stepKernel, ← h_step,
+  rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h_step h_action ⊢
+  rw [h_action, ← Measure.compProd_assoc, ← stepKernel, ← h_step,
     Measure.map_map (by fun_prop) (by fun_prop)]
   rfl
 
@@ -182,7 +229,7 @@ lemma condDistrib_reward_zero [StandardBorelSpace R] [Nonempty R]
       =ᵐ[(trajMeasure alg env).map (action 0)] env.ν0 := by
   have h_step := (hasLaw_step_zero alg env).map_eq
   have h_action := (hasLaw_action_zero alg env).map_eq
-  rwa [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop), h_action]
+  rwa [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop), h_action]
 
 section DetAlgorithm
 
@@ -209,39 +256,6 @@ lemma action_zero_detAlgorithm [MeasurableSingletonClass α] : action 0 =ᵐ[
     simp [detAlgorithm]
   exact ae_of_ae_map (by fun_prop) h_eq
 
-lemma action_eq_eval_comp_hist (n : ℕ) :
-    action (α := α) (R := R) n = (fun x ↦ (x ⟨n, by simp⟩).1) ∘ (hist n) := rfl
-
-lemma reward_eq_eval_comp_hist (n : ℕ) :
-    reward (α := α) (R := R) n = (fun x ↦ (x ⟨n, by simp⟩).2) ∘ (hist n) := rfl
-
-lemma measurable_hist_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (hist n) := by
-  simp [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe,
-    measurable_iff_comap_le]
-
--- todo: due to the type of `Adapted` and the fact that `Iic n → α × R` depends on `n`, we cannot
--- state that `hist` is adapted.
-
-lemma measurable_action_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (action n) := by
-  simp only [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe]
-  rw [action_eq_eval_comp_hist]
-  exact measurable_comp_comap _ (by fun_prop)
-
-lemma adapted_action [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
-    [SecondCountableTopology α] [OpensMeasurableSpace α] :
-    Adapted (Learning.filtration α R) action :=
-  fun n ↦ (measurable_action_filtration n).stronglyMeasurable
-
-lemma measurable_reward_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (reward n) := by
-  simp only [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe]
-  rw [reward_eq_eval_comp_hist]
-  exact measurable_comp_comap _ (by fun_prop)
-
-lemma adapted_reward [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R]
-    [SecondCountableTopology R] [OpensMeasurableSpace R] :
-    Adapted (Learning.filtration α R) reward :=
-  fun n ↦ (measurable_reward_filtration n).stronglyMeasurable
-
 lemma action_detAlgorithm_ae_eq
     [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
     (n : ℕ) :
@@ -275,13 +289,13 @@ lemma condDistrib_reward_stationaryEnv [StandardBorelSpace α] [Nonempty α]
     condDistrib (reward n) (action n) 𝔓 =ᵐ[(𝔓).map (action n)] ν := by
   cases n with
   | zero =>
-    rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)]
+    rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)]
     change (𝔓).map (step 0) = (𝔓).map (action 0) ⊗ₘ ν
     rw [(hasLaw_action_zero alg (stationaryEnv ν)).map_eq,
       (hasLaw_step_zero alg (stationaryEnv ν)).map_eq, stationaryEnv_ν0]
   | succ n =>
     have h_eq := condDistrib_reward alg (stationaryEnv ν) n
-    rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)] at h_eq ⊢
+    rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h_eq ⊢
     have : (𝔓).map (action (n + 1)) = ((𝔓).map (fun x ↦ (hist n x, action (n + 1) x))).snd := by
       rw [Measure.snd_map_prodMk (by fun_prop)]
     simp only [stationaryEnv_feedback] at h_eq

LeanBandits/Bandit.lean

@@ -6,7 +6,6 @@ Authors: Rémy Degenne, Paulo Rauber
 import Mathlib
 import LeanBandits.Algorithm
 import LeanBandits.ForMathlib.CondDistrib
-import LeanBandits.ForMathlib.KernelCompositionLemmas
 import LeanBandits.ForMathlib.Traj
 
 /-!
@@ -196,6 +195,8 @@ protected def filtration (α R : Type*) [MeasurableSpace α] [MeasurableSpace R]
     Filtration ℕ (inferInstance : MeasurableSpace (ℕ → α × R)) :=
   MeasureTheory.Filtration.piLE (X := fun _ ↦ α × R)
 
+section Laws
+
 lemma hasLaw_step_zero (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] :
     HasLaw (fun h : ℕ → α × R ↦ h 0) (alg.p0 ⊗ₘ ν) (Bandit.trajMeasure alg ν) :=
   Learning.hasLaw_step_zero alg (stationaryEnv ν)
@@ -236,32 +237,32 @@ lemma condIndepFun_reward_hist_arm [StandardBorelSpace α] [Nonempty α]
       (measurable_arm _).comap_le (reward (n + 1)) (hist n) (Bandit.trajMeasure alg ν) :=
   Learning.condIndepFun_reward_hist_action n
 
+end Laws
+
 section DetAlgorithm
 
 variable {nextArm : (n : ℕ) → (Iic n → α × R) → α} {h_next : ∀ n, Measurable (nextArm n)}
   {arm0 : α} {ν : Kernel α R} [IsMarkovKernel ν]
 
-lemma HasLaw_arm_zero_detAlgorithm :
-    HasLaw (arm 0) (Measure.dirac arm0)
-      (Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν) where
+local notation "𝔓t" => Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν
+
+lemma HasLaw_arm_zero_detAlgorithm : HasLaw (arm 0) (Measure.dirac arm0) 𝔓t where
   map_eq := (hasLaw_arm_zero _ _).map_eq
 
 lemma arm_zero_detAlgorithm [MeasurableSingletonClass α] :
-    arm 0 =ᵐ[Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν] fun _ ↦ arm0 := by
-  have h_eq : ∀ᵐ x ∂((Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν).map (arm 0)), x
-      = arm0 := by
+    arm 0 =ᵐ[𝔓t] fun _ ↦ arm0 := by
+  have h_eq : ∀ᵐ x ∂(((𝔓t).map (arm 0))), x = arm0 := by
     rw [(hasLaw_arm_zero _ _).map_eq]
     simp [detAlgorithm]
   exact ae_of_ae_map (by fun_prop) h_eq
 
 lemma arm_detAlgorithm_ae_eq (n : ℕ) :
-    arm (n + 1) =ᵐ[Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν]
-      fun h ↦ nextArm n (fun i ↦ h i) := by
+    arm (n + 1) =ᵐ[𝔓t] fun h ↦ nextArm n (fun i ↦ h i) := by
+  -- rhs equals nextArm n ∘ hist n
   sorry
 
 example [MeasurableSingletonClass α] :
-    ∀ᵐ h ∂(Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν),
-    arm 0 h = arm0 ∧ ∀ n, arm (n + 1) h = nextArm n (fun i ↦ h i) := by
+    ∀ᵐ h ∂(𝔓t), arm 0 h = arm0 ∧ ∀ n, arm (n + 1) h = nextArm n (fun i ↦ h i) := by
   rw [eventually_and, ae_all_iff]
   exact ⟨arm_zero_detAlgorithm, arm_detAlgorithm_ae_eq⟩