Docstrings

LeanMachineLearning/Bandit/Bandit.lean

@@ -16,7 +16,25 @@ public import Mathlib.Probability.Independence.Integration
 public import Mathlib.Probability.Kernel.Representation
 
 /-!
-# Bandit
+# Array-of-rewards probability space for stochastic bandits
+
+We build a particular probability space for stochastic bandits, called the "array model", in which
+an infinite array of i.i.d. rewards is first produced for all actions. When the algorithm chooses
+action `a` for the `n`th time, it receives the reward in the row `a` of the array and column `n`.
+
+Some statements about bandit algorithms are easier to prove in this space, and can then be
+transfered to any other probability space using the fact that the conditinonal distributions of the
+arms and rewards specified in the bandit model determine their laws uniquely.
+
+## Main definitions
+
+* `streamMeasure ν`: probability measure on the space of infinite arrays of rewards,
+  where the rewards in each row are i.i.d. according to `ν`.
+* `probSpace α R`: probability space for the array model of stochastic bandits with action space `α`
+  and reward space `R`.
+* `arrayMeasure ν`: probability measure on `probSpace α R` for the array model of stochastic bandits
+  with reward kernel `ν`.
+
 -/
 
 @[expose] public section

home_page/Gemfile

@@ -0,0 +1,25 @@
+source "https://rubygems.org"
+
+# To upgrade, run `bundle update github-pages`.
+gem "github-pages", group: :jekyll_plugins
+# If you have any plugins, put them here!
+group :jekyll_plugins do
+  #gem "jekyll-feed", "~> 0.12"
+end
+
+# Windows and JRuby does not include zoneinfo files, so bundle the tzinfo-data gem
+# and associated library.
+platforms :mingw, :x64_mingw, :mswin, :jruby do
+  gem "tzinfo", "~> 1.2"
+  gem "tzinfo-data"
+end
+
+# Performance-booster for watching directories on Windows.
+gem "wdm", "~> 0.1.1", :platforms => [:mingw, :x64_mingw, :mswin]
+
+# Lock `http_parser.rb` gem to `v0.6.x` on JRuby builds since newer versions of the gem
+# do not have a Java counterpart.
+gem "http_parser.rb", "~> 0.6.0", :platforms => [:jruby]
+
+# Used for locally serving the website.
+gem "webrick", "~> 1.7"

home_page/_config.yml

@@ -0,0 +1,34 @@
+# Welcome to Jekyll!
+#
+# This config file is meant for settings that affect your whole blog, values
+# which you are expected to set up once and rarely edit after that. If you find
+# yourself editing this file very often, consider using Jekyll's data files
+# feature for the data you need to update frequently.
+#
+# For technical reasons, this file is *NOT* reloaded automatically when you use
+# 'bundle exec jekyll serve'. If you change this file, please restart the server process.
+#
+# If you need help with YAML syntax, here are some quick references for you:
+# https://learn-the-web.algonquindesign.ca/topics/markdown-yaml-cheat-sheet/#yaml
+# https://learnxinyminutes.com/docs/yaml/
+#
+# Site settings
+# These are used to personalize your new site. If you look in the HTML files,
+# you will see them accessed via {{ site.title }}, {{ site.email }}, and so on.
+# You can create any custom variable you would like, and they will be accessible
+# in the templates via {{ site.myvariable }}.
+
+title: Lean Machine Learning
+#email: your-email@example.com
+description: The Lean library for machine learning research.
+baseurl: "" # the subpath of your site, e.g. /blog
+url: "https://RemyDegenne.github.io/lean-bandits" # the base hostname & protocol for your site, e.g. http://example.com
+twitter_username:
+github_username: RemyDegenne
+repository: RemyDegenne/lean-bandits
+
+# Build settings
+remote_theme: pages-themes/cayman@v0.2.0
+plugins:
+  - jekyll-remote-theme
+  - jekyll-github-metadata

website/Main.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: David Thrane Christiansen
--/
 import VersoBlog
 
 import Site

website/Site.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: David Thrane Christiansen
--/
 import Site.FrontPage
 import Site.Roadmap
 import Site.Meta

website/Site/FrontPage.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: David Thrane Christiansen
--/
 import VersoBlog
 import Site.Meta
 

website/Site/Meta.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: David Thrane Christiansen
--/
 import VersoBlog
 
 open Verso Genre Blog Site Output Html Template Theme

website/Site/Roadmap.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Rémy Degenne
--/
 import VersoBlog
 import Site.Meta