Update to v4.33.0-rc2

LeanMachineLearning.lean

@@ -1,6 +1,5 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
-public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.Polish.StandardBorel
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Measurable
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.AbsolutelyContinuous
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.Lattice

LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean

@@ -5,7 +5,6 @@ Authors: Rémy Degenne, Paulo Rauber
 -/
 module
 
-public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.Polish.StandardBorel
 public import LeanMachineLearning.ForMathlib.Probability.Independence.CondIndepFun
 public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepFun
 public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepInfinitePi

LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean

@@ -109,7 +109,7 @@ theorem action_tendsto_any (h : IsAlgEnvSeq A Y (randomSampling μ) (evalEnv f h
     exact (Metric.measure_ball_pos μ a hε).ne'
   · intro n
     refine measure_mono ?_
-    simp only [mem_Iic, Set.subset_iInter_iff, Set.setOf_subset_setOf]
+    simp only [mem_Iic, Set.subset_iInter_iff, Set.ofPred_subset_ofPred]
     intro i hi ω (hω : ε ≤ (fun (j : Iic n) ↦ dist (A j.1 ω) a).min)
     simp_all only [univ_eq_attach, le_inf'_iff, mem_attach, forall_const, Subtype.forall, mem_Iic]
 
@@ -127,7 +127,7 @@ lemma image_action_tendsto_any
   refine action_tendsto_any h a hδ |> tendsto_zero_of_le <| ?_
   intro n
   refine measure_mono ?_
-  simp only [Set.setOf_subset_setOf]
+  simp only [Set.ofPred_subset_ofPred]
   intro ω hω
   rw [← argmin_spec]
   set j := argmin (fun (i : Iic n) ↦ dist (A i.1 ω) a)
@@ -162,7 +162,7 @@ lemma tendsto_min₀ (h : IsAlgEnvSeq A R (randomSampling μ) (evalEnv f hfc.mea
   refine image_action_tendsto_any hfc h a hε |> tendsto_zero_of_le <| ?_
   intro n
   refine measure_mono ?_
-  simp only [Set.setOf_subset_setOf]
+  simp only [Set.ofPred_subset_ofPred]
   intro ω hω
   rw [← argmin_spec]
   set j := argmin (fun (i : Iic n) ↦ dist (f (A i ω)) (f a))
@@ -191,7 +191,7 @@ lemma tendsto_max₀ (h : IsAlgEnvSeq A R (randomSampling μ) (evalEnv f hfc.mea
   refine image_action_tendsto_any hfc h a hε |> tendsto_zero_of_le <| ?_
   intro n
   refine measure_mono ?_
-  simp only [Set.setOf_subset_setOf]
+  simp only [Set.ofPred_subset_ofPred]
   intro ω hω
   rw [← argmin_spec]
   set j := argmin (fun (i : Iic n) ↦ dist (f (A i ω)) (f a))

LeanMachineLearning/SequentialLearning/StationaryEnv.lean

@@ -191,11 +191,18 @@ variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
 
 namespace IsAlgEnvSeq
 
+/-- The conditional distribution of the feedback at time `n` given the action at time `n`
+is `ν n`. -/
+lemma hasCondDistrib_feedback_obliviousEnv {ν : ℕ → Kernel 𝓐 𝓨} [∀ n, IsMarkovKernel (ν n)]
+    (h : IsAlgEnvSeq A Y alg (obliviousEnv ν) P) (n : ℕ) :
+    HasCondDistrib (Y n) (A n) (ν n) P := by
+  simpa using IsObliviousEnv.hasCondDistrib_feedback h n
+
 /-- The conditional distribution of the feedback at time `n` given the action at time `n` is `ν`. -/
 lemma hasCondDistrib_feedback_stationaryEnv
     (h : IsAlgEnvSeq A Y alg (stationaryEnv ν) P) (n : ℕ) :
-    HasCondDistrib (Y n) (A n) ν P := by
-  simpa using IsObliviousEnv.hasCondDistrib_feedback h n
+    HasCondDistrib (Y n) (A n) ν P :=
+  hasCondDistrib_feedback_obliviousEnv h n
 
 /-- The conditional distribution of the feedback at time `n` given the action at time `n` is `ν`. -/
 lemma condDistrib_feedback_stationaryEnv [StandardBorelSpace 𝓨] [Nonempty 𝓨]

lake-manifest.json

@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "18f56bef5344cefb0563662c495e3eb3824a2589",
+   "rev": "51e6992efd06126df61a496bebf8f49482a4e129",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "18f56bef5344cefb0563662c495e3eb3824a2589",
+   "inputRev": "v4.33.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6af30619664960f9c816b27157dff3ceb1500dcf",
+   "rev": "755ccbe968ad1b0255bee8b46d9cb2306486d6d8",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.33.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0",
+   "rev": "123d15766ba49356c02ebad2a4462dfe12d79899",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715",
+   "rev": "f5c090429dff3cf66cb65562526c9ea6e8edfbcb",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c",
+   "rev": "bb3469a87774349fe01898d8bf2fc6a1ce6411ca",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69",
+   "rev": "222c58dad7706a6e7cae46c0edd65ea881d3ee27",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "57d3325be72a842920813bcb40f96a6f7393c185",
+   "rev": "7db8190085343afde2f5d2cdcc9bac719b6ec02c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d",
+   "rev": "ef42f8944eaf5b6cbfbe75d1917d824c7dd6cf33",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0ecf8993df88c044962426c2cbca0de5717d6150",
+   "rev": "76e1c118b0700b4ceafe99532e887d6431625e1a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "56958b3901ca108830de34fbce6cecd4b5757c1f",
+   "rev": "006dc1d1db18c5dc73d637c926cf132e88df05b5",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d",
+   "rev": "4343da18d95390b09fde98efb18125677c4b500c",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -125,10 +125,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf",
+   "rev": "1319485273bf87833fa472afbcefdedecb16b45f",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0-rc1",
+   "inputRev": "v4.33.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "LeanMachineLearning",

lakefile.toml

@@ -12,12 +12,12 @@ weak.linter.mathlibStandardSet = true
 [[require]]
 name = "verso"
 git = "https://github.com/leanprover/verso"
-rev = "main"
+rev = "v4.33.0-rc2"
 
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "18f56bef5344cefb0563662c495e3eb3824a2589"
+rev = "v4.33.0-rc2"
 
 [[lean_lib]]
 name = "LeanMachineLearning"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.33.0-rc1
+leanprover/lean4:v4.33.0-rc2