CI fix attempt

.github/workflows/blueprint.yml

@@ -58,7 +58,18 @@ jobs:
       - name: Compile blueprint and documentation
         uses: leanprover-community/docgen-action@deed0cdc44dd8e5de07a300773eb751d33e32fc8 # 2025-10-26
         with:
+          homepage: home_page
           blueprint: true
-          api-docs: false
           build-page: false
-          homepage: home_page
+          deploy: false
+
+      - name: "Upload website (API documentation, blueprint and any home page)"
+        if: github.event_name == 'push'
+        uses: actions/upload-pages-artifact@56afc609e74202658d3ffba0e8f6dda462b719fa # v3.0.1
+        with:
+          path: home_page/
+
+      - name: Deploy to GitHub Pages
+        if: github.event_name == 'push'
+        id: deployment
+        uses: actions/deploy-pages@d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e # v4.0.5

LeanMachineLearning/Bandit/Regret.lean

@@ -10,6 +10,14 @@ public import LeanMachineLearning.SequentialLearning.FiniteActions
 /-!
 # Regret, gap, best arm
 
+## Main definitions
+
+* `gap ν a` is the gap of an action `a`, i.e., the difference between the highest mean of the
+  actions and the mean of `a`.
+* `regret ν A t ω` is the regret of a sequence of pulls `A : ℕ → Ω → α` at time `t` for the reward
+  kernel `ν : Kernel α ℝ` and the outcome `ω : Ω`.
+* `bestArm ν` is an action with the highest mean.
+
 -/
 
 @[expose] public section