feat: require Statlib, bump Mathlib to 2ddf59c

.github/workflows/update.yml

@@ -6,34 +6,57 @@ on:
   workflow_dispatch:
 
 jobs:
-  bump:
+  # LML gets Mathlib through Statlib: bumping Statlib to its latest `main` commit also moves Mathlib
+  # (and Mathlib's dependencies) to the commits that Statlib pins. Statlib keeps itself close to
+  # Mathlib master with its own updater, and the incompatibilities with Mathlib are tracked there.
+  bump-statlib:
     runs-on: ubuntu-latest
     permissions:
       contents: write
       pull-requests: write
     steps:
       - uses: actions/checkout@v7
 
-      - name: Bump to latest mathlib
+      - name: Install Lean
+        uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
+        with:
+          auto-config: false
+          use-mathlib-cache: false
+
+      - name: Bump Statlib
         id: bump
-        uses: leanprover-community/downstream-reports/.github/actions/bump-to-latest@main
+        run: |
+          rev() { jq -r --arg name "$1" '.packages[] | select(.name == $name) | .rev' lake-manifest.json; }
+          old=$(rev Statlib)
+          lake update Statlib
+          new=$(rev Statlib)
+          if [ "$old" = "$new" ]; then
+            echo "Statlib is already at its latest commit ${new:0:7}."
+            echo "updated=false" >> "$GITHUB_OUTPUT"
+            exit 0
+          fi
+          mathlib=$(rev mathlib)
+          {
+            echo "updated=true"
+            echo "title=chore: bump Statlib to ${new:0:7} (Mathlib ${mathlib:0:7})"
+          } >> "$GITHUB_OUTPUT"
+
+      # Pull requests opened by this workflow do not trigger the Build workflow, so the bump is
+      # checked here, and opened only if LML and its tutorial build without warnings.
+      - name: Build
+        if: steps.bump.outputs.updated == 'true'
+        run: |
+          lake exe cache get
+          lake build --wfail LeanMachineLearning LMLTutorial
 
       - name: Open or update PR
         if: steps.bump.outputs.updated == 'true'
         uses: leanprover-community/downstream-reports/.github/actions/open-bump-pr@main
         with:
-          title:          ${{ steps.bump.outputs.pr-title }}
-          message:        ${{ steps.bump.outputs.bump-description }}
-          commit-message: ${{ steps.bump.outputs.commit-message }}
-
-  open-issue:
-    runs-on: ubuntu-latest
-    permissions:
-      issues: write
-      contents: write
-      pull-requests: write
-    steps:
-      - uses: actions/checkout@v7
-
-      - name: Open or update incompatibility issue and PR
-        uses: leanprover-community/downstream-reports/.github/actions/track-incompatibility@main
+          branch:         statlib-bump
+          title:          ${{ steps.bump.outputs.title }}
+          commit-message: ${{ steps.bump.outputs.title }}
+          body: >
+            Bumps Statlib to its latest `main` commit. LML gets Mathlib through Statlib, so Mathlib
+            moves to the commit that Statlib pins. `lake build --wfail LeanMachineLearning
+            LMLTutorial` passed in the workflow run that opened this pull request.

LMLTutorial/Pages/Martingales.lean

@@ -91,7 +91,7 @@ This is the Mathlib lemma `Submartingale.ae_tendsto_limitProcess`.
 
 ```lean
 example {Y : ℕ → Ω → ℝ} (hY : Submartingale Y 𝓕 P)
-    {R : ℝ≥0} (hbdd : ∀ n, eLpNorm (Y n) 1 P ≤ R) :
+    (hbdd : ⨆ n, eLpNorm (Y n) 1 P < ∞) :
     ∀ᵐ ω ∂P, Tendsto (Y · ω) atTop (𝓝 (𝓕.limitProcess Y P ω)) :=
   hY.ae_tendsto_limitProcess hbdd
 ```

LeanMachineLearning.lean

@@ -6,9 +6,7 @@ public import LeanMachineLearning.ForMathlib.Analysis.Convex.Integral
 public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Basic
 public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv
 public import LeanMachineLearning.ForMathlib.Basic.Unique
-public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.ChainRule
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.CompProd
-public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Convex
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.DataProcessing
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.MapSequence
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Restrict
@@ -46,7 +44,6 @@ public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.Meas
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.WithDensity
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.CondDistrib
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.IonescuTulcea.Traj
-public import LeanMachineLearning.ForMathlib.Probability.Kernel.MeasurableSpace
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.RadonNikodym
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Sigma
 public import LeanMachineLearning.ForMathlib.Probability.Moments.SubExponential