Update dependencies

LeanBandits/Bandit/Regret.lean

@@ -26,7 +26,7 @@ noncomputable
 def gap (ν : Kernel α ℝ) (a : α) : ℝ := (⨆ i, (ν i)[id]) - (ν a)[id]
 
 omit [DecidableEq α] in
-lemma gap_nonneg [Fintype α] : 0 ≤ gap ν a := by
+lemma gap_nonneg [Finite α] : 0 ≤ gap ν a := by
   rw [gap, sub_nonneg]
   exact le_ciSup (f := fun i ↦ (ν i)[id]) (by simp) a
 
@@ -40,12 +40,12 @@ lemma regret_eq_sum_gap : regret ν A t ω = ∑ s ∈ range t, gap ν (A s ω)
   simp [regret, gap]
 
 omit [DecidableEq α] in
-lemma regret_nonneg [Fintype α] : 0 ≤ regret ν A t ω := by
+lemma regret_nonneg [Finite α] : 0 ≤ regret ν A t ω := by
   rw [regret_eq_sum_gap]
   exact sum_nonneg (fun _ _ ↦ gap_nonneg)
 
 omit [DecidableEq α] in
-lemma gap_eq_zero_of_regret_eq_zero [Fintype α] (hr : regret ν A t ω = 0) {s : ℕ} (hs : s < t) :
+lemma gap_eq_zero_of_regret_eq_zero [Finite α] (hr : regret ν A t ω = 0) {s : ℕ} (hs : s < t) :
     gap ν (A s ω) = 0 := by
   rw [regret_eq_sum_gap] at hr
   exact (sum_eq_zero_iff_of_nonneg fun _ _ ↦ gap_nonneg).1 hr s (mem_range.2 hs)
@@ -130,9 +130,10 @@ lemma avg_mean_reward_tendsto_of_sublinear_regret
   ring
 
 /-- If the regret is sublinear, the rate of suboptimal arm pulls tends to zero. -/
-lemma pullCount_rate_tendsto_of_sublinear_regret [Fintype α]
+lemma pullCount_rate_tendsto_of_sublinear_regret [Finite α]
     (hr : (regret ν A · ω) =o[atTop] fun t ↦ (t : ℝ)) (hg : 0 < gap ν a) :
     Tendsto (fun t ↦ (pullCount A a t ω : ℝ) / t) atTop (nhds 0) := by
+  have := Fintype.ofFinite α
   have hb (t : ℕ) : (pullCount A a t ω : ℝ) * gap ν a ≤ regret ν A t ω := by
     rw [regret_eq_sum_pullCount_mul_gap]
     exact single_le_sum (f := fun a ↦ pullCount A a t ω * gap ν a)

LeanBandits/ForMathlib/CondDistrib.lean

@@ -457,7 +457,7 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
         · simp only [hZ, Set.setOf_true, Set.mem_setOf_eq, Set.indicator_of_mem]
           exact κ.measure_le_bound _ _
         · simp [hZ]
-      refine le_antisymm (h_le.trans ?_) zero_le'
+      refine le_antisymm (h_le.trans ?_) (zero_le _)
       rw [lintegral_indicator]
       swap; · exact (measurableSet_singleton _).preimage (by fun_prop)
       simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter,

LeanBandits/SequentialLearning/Algorithm.lean

@@ -183,66 +183,41 @@ def IsAlgEnvSeq.filtration (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurab
     rw [← measurable_iff_comap_le]
     exact measurable_hist hA hR' i
 
-lemma IsAlgEnvSeq.measurable_hist_filtration
-    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (n : ℕ) :
-    Measurable[IsAlgEnvSeq.filtration hA hR' n] (IsAlgEnvSeq.hist A R' n) :=
-  measurable_iff_comap_le.mpr le_rfl
-
-lemma IsAlgEnvSeq.adapted_hist [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
-    [SecondCountableTopology α] [OpensMeasurableSpace α]
-    [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R]
-    [SecondCountableTopology R] [OpensMeasurableSpace R]
+lemma IsAlgEnvSeq.adapted_hist
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) :
     Adapted (filtration hA hR') (IsAlgEnvSeq.hist A R') :=
-  fun n ↦ (IsAlgEnvSeq.measurable_hist_filtration hA hR' n).stronglyMeasurable
+  fun _ ↦ measurable_iff_comap_le.mpr le_rfl
 
-lemma IsAlgEnvSeq.measurable_step_filtration
-    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (n : ℕ) :
-    Measurable[IsAlgEnvSeq.filtration hA hR' n] (IsAlgEnvSeq.step A R' n) := by
+lemma IsAlgEnvSeq.adapted_step
+    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) :
+    Adapted (filtration hA hR') (step A R') := by
+  intro n
   have : step A R' n = (fun h ↦ (h ⟨n, by simp⟩)) ∘ (hist A R' n) := by
     ext ω : 1
     simp [hist, step]
   rw [this]
   exact measurable_comp_comap _ (by fun_prop)
 
-lemma IsAlgEnvSeq.adapted_step [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
-    [SecondCountableTopology α] [OpensMeasurableSpace α]
-    [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R]
-    [SecondCountableTopology R] [OpensMeasurableSpace R]
+lemma IsAlgEnvSeq.adapted_action
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) :
-    Adapted (filtration hA hR') (step A R') :=
-  fun n ↦ (IsAlgEnvSeq.measurable_step_filtration hA hR' n).stronglyMeasurable
-
-lemma IsAlgEnvSeq.measurable_action_filtration
-    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (n : ℕ) :
-    Measurable[IsAlgEnvSeq.filtration hA hR' n] (A n) := by
+    Adapted (filtration hA hR') A := by
+  intro n
   have : A n = (fun h ↦ (h ⟨n, by simp⟩).1) ∘ (hist A R' n) := by
     ext ω : 1
     simp [IsAlgEnvSeq.hist]
   rw [this]
   exact measurable_comp_comap _ (by fun_prop)
 
-lemma IsAlgEnvSeq.adapted_action [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
-    [SecondCountableTopology α] [OpensMeasurableSpace α]
+lemma IsAlgEnvSeq.adapted_reward
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) :
-    Adapted (filtration hA hR') A :=
-  fun n ↦ (IsAlgEnvSeq.measurable_action_filtration hA hR' n).stronglyMeasurable
-
-lemma IsAlgEnvSeq.measurable_reward_filtration
-    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (n : ℕ) :
-    Measurable[IsAlgEnvSeq.filtration hA hR' n] (R' n) := by
+    Adapted (filtration hA hR') R' := by
+  intro n
   have : R' n = (fun h ↦ (h ⟨n, by simp⟩).2) ∘ (hist A R' n) := by
     ext ω : 1
     simp [IsAlgEnvSeq.hist]
   rw [this]
   exact measurable_comp_comap _ (by fun_prop)
 
-lemma IsAlgEnvSeq.adapted_reward [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R]
-    [SecondCountableTopology R] [OpensMeasurableSpace R]
-    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) :
-    Adapted (filtration hA hR') R' :=
-  fun n ↦ (IsAlgEnvSeq.measurable_reward_filtration hA hR' n).stronglyMeasurable
-
 /-- Filtration generated by the history at time `n-1` together with the action at time `n`. -/
 def IsAlgEnvSeq.filtrationAction
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) :
@@ -259,7 +234,7 @@ def IsAlgEnvSeq.filtrationAction
         rw [← measurable_iff_comap_le]
         suffices Measurable[IsAlgEnvSeq.filtration hA hR' 0] (A 0) from
           this.mono ((IsAlgEnvSeq.filtration hA hR').mono zero_le') le_rfl
-        exact measurable_action_filtration hA hR' 0
+        exact adapted_action hA hR' 0
     have hm : m ≠ 0 := by grind
     simp only [hn, hm, ↓reduceIte]
     have hnm' : n - 1 ≤ m - 1 := by grind
@@ -274,7 +249,7 @@ def IsAlgEnvSeq.filtrationAction
       have h_le : n ≤ m - 1 := by grind
       suffices Measurable[IsAlgEnvSeq.filtration hA hR' n] (A n) from
         this.mono ((IsAlgEnvSeq.filtration hA hR').mono h_le) le_rfl
-      exact measurable_action_filtration hA hR' n
+      exact adapted_action hA hR' n
   le' n := by
     by_cases hn : n = 0
     · simp only [hn, ↓reduceIte]

LeanBandits/SequentialLearning/FiniteActions.lean

@@ -207,26 +207,22 @@ lemma measurable_uncurry_pullCount' [MeasurableEq α] (n : ℕ) :
     exact measurableSet_eq_fun (by fun_prop) (by fun_prop)
   fun_prop
 
-lemma adapted_pullCount_add_one' [MeasurableSingletonClass α]
-    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : α) (n : ℕ) :
-    Measurable[IsAlgEnvSeq.filtration hA hR' n] (pullCount A a (n + 1)) := by
+lemma adapted_pullCount_add_one [MeasurableSingletonClass α]
+    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : α) :
+    Adapted (IsAlgEnvSeq.filtration hA hR') (fun n ↦ pullCount A a (n + 1)) := by
+  intro n
   have : pullCount A a (n + 1) = (fun h : Iic n → α × R ↦ pullCount' n h a) ∘
       (IsAlgEnvSeq.hist A R' n) := by
     ext
     exact pullCount_add_one_eq_pullCount'
-  rw [IsAlgEnvSeq.filtration, this]
+  simp_rw [IsAlgEnvSeq.filtration, this]
   exact measurable_comp_comap _ (measurable_pullCount' n a)
 
-lemma adapted_pullCount_add_one [MeasurableSingletonClass α]
-    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : α) :
-    Adapted (IsAlgEnvSeq.filtration hA hR') (fun n ↦ pullCount A a (n + 1)) :=
-  fun n ↦ Measurable.stronglyMeasurable <| adapted_pullCount_add_one' hA hR' a n
-
 lemma isPredictable_pullCount [MeasurableSingletonClass α]
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : α) :
     IsPredictable (IsAlgEnvSeq.filtration hA hR') (pullCount A a) := by
   rw [isPredictable_iff_measurable_add_one]
-  refine ⟨?_, fun n ↦ (adapted_pullCount_add_one hA hR' a n).measurable⟩
+  refine ⟨?_, adapted_pullCount_add_one hA hR' a⟩
   simp only [pullCount_zero]
   fun_prop
 
@@ -511,9 +507,10 @@ lemma isStoppingTime_stepsUntil [MeasurableSingletonClass α]
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : α) (hm : m ≠ 0) :
     IsStoppingTime (IsAlgEnvSeq.filtration hA hR') (stepsUntil A a m) := by
   rw [stepsUntil_eq_leastGE _ hm]
-  refine Adapted.isStoppingTime_leastGE _ fun n ↦ ?_
+  refine StronglyAdapted.isStoppingTime_leastGE _ fun n ↦ ?_
   suffices StronglyMeasurable[IsAlgEnvSeq.filtration hA hR' n] (pullCount A a (n + 1)) by
     fun_prop
+  refine Measurable.stronglyMeasurable ?_
   exact adapted_pullCount_add_one hA hR' a n
 
 -- todo: get this from the stopping time property?
@@ -592,8 +589,8 @@ lemma measurable_comap_indicator_stepsUntil_eq [MeasurableSingletonClass α]
     by_cases hn : n = 0
     · simp only [hn, pullCount_zero]
       exact measurable_const
-    have h_meas := adapted_pullCount_add_one' hA hR' a (n - 1)
-    rwa [Nat.sub_add_cancel (by lia)] at h_meas
+    have h_meas := adapted_pullCount_add_one hA hR' a (n - 1)
+    grind
 
 lemma measurable_indicator_stepsUntil_eq [MeasurableSingletonClass α]
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : α) (m n : ℕ) :
@@ -880,11 +877,11 @@ lemma IsAlgEnvSeq.isPredictable_sumRewards [StandardBorelSpace α] [Nonempty α]
     fun_prop
   refine fun n ↦ measurable_fun_sum _ fun i hi ↦ Measurable.ite ?_ ?_ (by fun_prop)
   · refine (measurableSet_singleton a).preimage ?_
-    have h_meas_i := IsAlgEnvSeq.measurable_action_filtration h.measurable_A h.measurable_R i
+    have h_meas_i := IsAlgEnvSeq.adapted_action h.measurable_A h.measurable_R i
     simp only [mem_range] at hi
     exact h_meas_i.mono ((IsAlgEnvSeq.filtration h.measurable_A h.measurable_R).mono (by lia))
       le_rfl
-  · have h_meas_i := IsAlgEnvSeq.measurable_reward_filtration h.measurable_A h.measurable_R i
+  · have h_meas_i := IsAlgEnvSeq.adapted_reward h.measurable_A h.measurable_R i
     simp only [mem_range] at hi
     exact h_meas_i.mono ((IsAlgEnvSeq.filtration h.measurable_A h.measurable_R).mono (by lia))
       le_rfl
@@ -896,7 +893,7 @@ lemma IsAlgEnvSeq.adapted_sumRewards_add_one [StandardBorelSpace α] [Nonempty 
       (fun n ↦ sumRewards A R' a (n + 1)) := by
   have h_predictable := h.isPredictable_sumRewards a
   rw [isPredictable_iff_measurable_add_one] at h_predictable
-  exact fun n ↦ Measurable.stronglyMeasurable (h_predictable.2 n)
+  exact h_predictable.2
 
 section CopiedFromPR
 
@@ -938,7 +935,7 @@ lemma IsAlgEnvSeq.adapted_empMean_add_one [StandardBorelSpace α] [Nonempty α]
       (fun n ↦ empMean A R' a (n + 1)) := by
   have h_predictable := h.isPredictable_empMean a
   rw [isPredictable_iff_measurable_add_one] at h_predictable
-  exact fun n ↦ Measurable.stronglyMeasurable (h_predictable.2 n)
+  exact h_predictable.2
 
 end SumRewards
 

LeanBandits/SequentialLearning/IonescuTulceaSpace.lean

@@ -86,45 +86,25 @@ lemma action_eq_eval_comp_hist (n : ℕ) :
 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[IT.filtration α R n] (step n) := by
+lemma adapted_step : Adapted (IT.filtration α R) (step (α := α) (R := R)) := by
+  intro n
   rw [filtration_eq_comap, 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 (IT.filtration α R) (step (α := α) (R := R)) :=
-  fun n ↦ (measurable_step_filtration n).stronglyMeasurable
-
-lemma measurable_hist_filtration (n : ℕ) : Measurable[IT.filtration α R n] (hist n) := by
+lemma adapted_hist : Adapted (IT.filtration α R) hist := by
+  intro n
   simp [filtration_eq_comap, measurable_iff_comap_le]
 
-lemma adapted_hist [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
-    [SecondCountableTopology α] [OpensMeasurableSpace α]
-    [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R]
-    [SecondCountableTopology R] [OpensMeasurableSpace R] :
-    Adapted (IT.filtration α R) hist :=
-  fun n ↦ (measurable_hist_filtration n).stronglyMeasurable
-
-lemma measurable_action_filtration (n : ℕ) : Measurable[IT.filtration α R n] (action n) := by
+lemma adapted_action : Adapted (IT.filtration α R) action := by
+  intro n
   rw [filtration_eq_comap, action_eq_eval_comp_hist]
   exact measurable_comp_comap _ (by fun_prop)
 
-lemma adapted_action [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
-    [SecondCountableTopology α] [OpensMeasurableSpace α] :
-    Adapted (IT.filtration α R) action :=
-  fun n ↦ (measurable_action_filtration n).stronglyMeasurable
-
-lemma measurable_reward_filtration (n : ℕ) : Measurable[IT.filtration α R n] (reward n) := by
+lemma adapted_reward : Adapted (IT.filtration α R) reward := by
+  intro n
   rw [filtration_eq_comap, 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 (IT.filtration α R) reward :=
-  fun n ↦ (measurable_reward_filtration n).stronglyMeasurable
-
 section FiltrationAction
 
 /-- Filtration generated by the history at time `n-1` together with the action at time `n`. -/
@@ -142,7 +122,7 @@ def filtrationAction (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] :
         rw [← measurable_iff_comap_le]
         suffices Measurable[IT.filtration α R 0] (action 0) from
           this.mono ((IT.filtration α R).mono zero_le') le_rfl
-        exact measurable_action_filtration 0
+        exact adapted_action 0
     have hm : m ≠ 0 := by grind
     simp only [hn, hm, ↓reduceIte]
     have hnm' : n - 1 ≤ m - 1 := by grind
@@ -157,7 +137,7 @@ def filtrationAction (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] :
       have h_le : n ≤ m - 1 := by grind
       suffices Measurable[IT.filtration α R n] (action n) from
         this.mono ((IT.filtration α R).mono h_le) le_rfl
-      exact measurable_action_filtration n
+      exact adapted_action n
   le' n := by
     by_cases hn : n = 0
     · simp only [hn, ↓reduceIte]
@@ -192,12 +172,12 @@ lemma filtrationAction_le_filtration_self (n : ℕ) :
   by_cases hn : n = 0
   · simp only [hn, filtrationAction_zero_eq_comap]
     rw [← measurable_iff_comap_le]
-    exact measurable_action_filtration 0
+    exact adapted_action 0
   simp only [filtrationAction, hn, ↓reduceIte, sup_le_iff]
   constructor
   · exact (IT.filtration α R).mono (by grind)
   · rw [← measurable_iff_comap_le]
-    exact measurable_action_filtration _
+    exact adapted_action _
 
 lemma filtrationAction_le_filtration {m n : ℕ} (h : m ≤ n) :
     filtrationAction α R m ≤ IT.filtration α R n :=

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "725c803ee924f55342e93f2c75976051ab902b54",
+   "rev": "62a82d6d0a3d3c54ca96bf00a861c623f3e0be44",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
+   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890",
+   "rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ef8377f31b5535430b6753a974d685b0019d0681",
+   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.84",
+   "inputRev": "v0.0.86",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c",
+   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72",
+   "rev": "23324752757bf28124a518ec284044c8db79fee5",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2e16f91af2a97975e5d2fac906494cd6c17ba255",
+   "rev": "ab9f3956f91980e61bea324c0cf1e9e7d9c8518b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
+   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0-rc1",
+   "inputRev": "v4.28.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "LeanBandits",