Update to v4.34.0

.github/workflows/build.yml

@@ -68,7 +68,7 @@ jobs:
       - name: Build the referee site
         id: referee
         if: github.event_name == 'push'
-        uses: LeanMachineLearning/exposition@v4.34.0-rc2-7
+        uses: LeanMachineLearning/exposition@v4.34.0
         with:
           root: LeanMachineLearning
           exclude-lib: LMLTutorial

LMLTutorial/Pages/DefiningAlgorithm.lean

@@ -7,6 +7,15 @@ module
 
 public import VersoManual
 public import LeanMachineLearning
+-- `import all` is needed to load the docstrings for the `{docstring}` blocks below.
+import all LeanMachineLearning.Online.Bandit.Algorithms.Regret.UCB
+import all LeanMachineLearning.Online.Bandit.Algorithms.UCB
+import all LeanMachineLearning.Online.Bandit.Regret
+import all LeanMachineLearning.SequentialLearning.Algorithm
+import all LeanMachineLearning.SequentialLearning.Deterministic
+import all LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
+import all LeanMachineLearning.SequentialLearning.StationaryEnv
+import all LeanMachineLearning.SequentialLearning.SumRewards
 
 set_option linter.style.header false
 set_option linter.style.setOption false

LeanMachineLearning/ForMathlib/Probability/Kernel/Composition/IntegralCompProd.lean

@@ -63,6 +63,6 @@ lemma norm_integral_rpow_le_integral_norm_rpow
     ConvexOn.map_integral_le (convexOn_rpow hp1')
       (Real.continuous_rpow_const (by positivity)).continuousOn isClosed_Ici
       (ae_of_all _ fun x ↦ norm_nonneg _) (hf.integrable hp1).norm
-      ((integrable_norm_rpow_iff hf.1 hp0 hp_top).mpr hf)
+      ((integrable_norm_rpow_iff hf.aestronglyMeasurable hp0 hp_top).mpr hf)
 
 end MeasureTheory

LeanMachineLearning/ForMathlib/Probability/Moments/SubExponential.lean

@@ -136,10 +136,11 @@ lemma ae_forall_integrable_exp_mul (h : HasSubexponentialMGF X V b κ ν) :
 lemma ae_forall_memLp_exp_mul (h : HasSubexponentialMGF X V b κ ν) (p : ℝ≥0) :
     ∀ᵐ ω' ∂ν, ∀ t : ℝ, b * |(p : ℝ) * t| ≤ 1 → MemLp (fun ω ↦ exp (t * X ω)) p (κ ω') := by
   filter_upwards [h.ae_forall_integrable_exp_mul, h.ae_aestronglyMeasurable] with ω' hi hm t ht
-  refine ⟨continuous_exp.comp_aestronglyMeasurable (hm.const_mul t), ?_⟩
+  have hmeas : AEStronglyMeasurable (fun ω ↦ exp (t * X ω)) (κ ω') :=
+    continuous_exp.comp_aestronglyMeasurable (hm.const_mul t)
   by_cases hp : p = 0
-  · simp [hp]
-  rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp) (by simp),
+  · simp [hp, hmeas]
+  rw [memLp_iff, eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp) (by simp) hmeas,
     ENNReal.coe_toReal]
   have hf := (hi (p * t) ht).lintegral_lt_top
   convert! hf using 3 with ω
@@ -150,10 +151,11 @@ lemma ae_forall_memLp_exp_mul (h : HasSubexponentialMGF X V b κ ν) (p : ℝ≥
 lemma memLp_exp_mul (h : HasSubexponentialMGF X V b κ ν) {t : ℝ} (p : ℝ≥0)
     (ht : b * |(p : ℝ) * t| ≤ 1) :
     MemLp (fun ω ↦ exp (t * X ω)) p (κ ∘ₘ ν) := by
-  refine ⟨continuous_exp.comp_aestronglyMeasurable (h.aestronglyMeasurable.const_mul t), ?_⟩
+  have hmeas : AEStronglyMeasurable (fun ω ↦ exp (t * X ω)) (κ ∘ₘ ν) :=
+    continuous_exp.comp_aestronglyMeasurable (h.aestronglyMeasurable.const_mul t)
   by_cases hp0 : p = 0
-  · simp [hp0]
-  rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp0) (by simp)]
+  · simp [hp0, hmeas]
+  rw [memLp_iff, eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp0) (by simp) hmeas]
   simp only [ENNReal.coe_toReal]
   have h' := (h.integrable_exp_mul (p * t) ht).2
   rw [hasFiniteIntegral_def] at h'

LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean

@@ -44,6 +44,7 @@ def UCB.nextArm (K : ℕ) [NeZero K] (c : ℝ) (n : ℕ) (h : Hist Unit (Fin K)
   if n < K then RoundRobin.nextAction K n else
   argmax (fun a ↦ empMean' n h a + ucbWidth' c n h a)
 
+/-- The next-arm function of UCB is measurable. -/
 @[fun_prop]
 lemma UCB.measurable_nextArm [NeZero K] (c : ℝ) (n : ℕ) : Measurable (nextArm K c n) := by
   unfold nextArm

lake-manifest.json

@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "217ba069a556ad9de837366b35c2ec1bec1de384",
+   "rev": "5ed2965256430c3649e86755f9576b54eca72435",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "217ba069a556ad9de837366b35c2ec1bec1de384",
+   "inputRev": "v4.34.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3bdedf29bada13d8103e6c979001c51dcee210c8",
+   "rev": "cad4b633e75ea769b851f12f9ca3b4f0dfcc625f",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0",
+   "inputRev": "v4.34.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d9598f07b1bc701f1e3aae163d2681c1fd978793",
+   "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ba67e212be1197b84c1f1f6299488a10a3002713",
+   "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1681d78dd6e65e38b143f9740d829c826673807c",
+   "rev": "e928b72544873815af278d38681b31c0293588e3",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f",
+   "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "18889deb9e83ea7420ef51c160d6f88552e744e3",
+   "rev": "355695d523e41d0554926416cba2a2b3544fbbc9",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3",
+   "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,17 +85,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4cac2177c37f5530c4da76aa8e4307f3fc9e4dcb",
+   "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.34.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/illuminate",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6bc815869cba1f19515715dc6b47795acd521f1c",
+   "rev": "a1a61c9678da010e958ed24cdfa6f635b85f172a",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -115,22 +125,12 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3a75ede05278806fd3249bb0c97a6fb5777a4f7d",
+   "rev": "9b90b7f938d6169246325df002351014f49945ef",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.34.0-rc2",
-   "inherited": true,
-   "configFile": "lakefile.toml"}],
+   "configFile": "lakefile.lean"}],
  "name": "LeanMachineLearning",
  "lakeDir": ".lake",
  "fixedToolchain": false}

lakefile.toml

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

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.34.0-rc2
+leanprover/lean4:v4.34.0