diff --git a/LeanMachineLearning/Bandit/Bandit.lean b/LeanMachineLearning/Bandit/Bandit.lean index e195a42a..8101f908 100644 --- a/LeanMachineLearning/Bandit/Bandit.lean +++ b/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 diff --git a/home_page/Gemfile b/home_page/Gemfile new file mode 100644 index 00000000..a6a5bb05 --- /dev/null +++ b/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" diff --git a/home_page/_config.yml b/home_page/_config.yml new file mode 100644 index 00000000..38559e00 --- /dev/null +++ b/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 diff --git a/website/Main.lean b/website/Main.lean index 18864a74..308259f3 100644 --- a/website/Main.lean +++ b/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 diff --git a/website/Site.lean b/website/Site.lean index b6c8a06d..20b33dad 100644 --- a/website/Site.lean +++ b/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 diff --git a/website/Site/FrontPage.lean b/website/Site/FrontPage.lean index 8fcee367..0e6ed2fd 100644 --- a/website/Site/FrontPage.lean +++ b/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 diff --git a/website/Site/Meta.lean b/website/Site/Meta.lean index d32a4a22..51604d59 100644 --- a/website/Site/Meta.lean +++ b/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 diff --git a/website/Site/Roadmap.lean b/website/Site/Roadmap.lean index 467f09d5..86cbeee6 100644 --- a/website/Site/Roadmap.lean +++ b/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