diff --git a/.github/workflows/blueprint.yml b/.github/workflows/build.yml similarity index 99% rename from .github/workflows/blueprint.yml rename to .github/workflows/build.yml index 4948b775..661935b6 100644 --- a/.github/workflows/blueprint.yml +++ b/.github/workflows/build.yml @@ -1,4 +1,4 @@ -name: Compile blueprint +name: Build on: push: @@ -356,7 +356,7 @@ jobs: run: | ./scripts/build_docs.sh - - name: Compile blueprint and documentation + - name: Build API documentation uses: leanprover-community/docgen-action@7b5b9a1822650bd45aaeb4182d94bceba2030f89 # 2026-04-14 with: homepage: home_page @@ -374,7 +374,7 @@ jobs: mkdir -p home_page/exposition cp -r referee-site/html-multi/. home_page/exposition/ - - name: "Upload website (API documentation, blueprint and any home page)" + - name: "Upload website (API documentation and home page)" if: github.event_name == 'push' uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v5.0.0 with: diff --git a/.gitignore b/.gitignore index acf454ad..a3a352df 100644 --- a/.gitignore +++ b/.gitignore @@ -1,17 +1,8 @@ -blueprint/src/print.pdf -blueprint/src/web.pdf - ## macOS .DS_Store ## Lake -.lake/* +.lake/ .cache/* -## Blueprint -/blueprint/print/print.log -/blueprint/web/ -/blueprint/src/web.paux -/blueprint/src/web.bbl -/blueprint/print/ ## TeX *.aux *.lof @@ -43,12 +34,5 @@ blueprint/src/web.pdf /exposition/ ## Tutorial and docs -/LMLTutorial/.lake/ /LMLTutorial/_out/ -/LMLDocs/.lake/ /LMLDocs/_out/ - -## Verso Blueprint -/verso_blueprint/.lake/ -/verso_blueprint/.build/ -/verso_blueprint/_out/ diff --git a/blueprint/lean_decls b/blueprint/lean_decls deleted file mode 100644 index dd0cdd5f..00000000 --- a/blueprint/lean_decls +++ /dev/null @@ -1,140 +0,0 @@ -Learning.Algorithm -Learning.Environment -Learning.detAlgorithm -Learning.stationaryEnv -Learning.IsAlgEnvSeq -Learning.IsAlgEnvSeq.hist -Learning.IsAlgEnvSeq.step -Learning.IsAlgEnvSeq.hasLaw_step_zero -Learning.IsAlgEnvSeq.hasCondDistrib_step -Learning.IsAlgEnvSeq.filtration -Learning.IsAlgEnvSeq.filtrationAction -Learning.IsAlgEnvSeq.adapted_step -Learning.IsAlgEnvSeq.adapted_hist -Learning.IsAlgEnvSeq.adapted_action -Learning.IsAlgEnvSeq.adapted_feedback -Learning.isAlgEnvSeq_unique -Learning.IsAlgEnvSeq.condDistrib_feedback_stationaryEnv -Learning.IsAlgEnvSeq.condIndepFun_feedback_hist_action -ProbabilityTheory.Kernel.traj -ProbabilityTheory.Kernel.trajMeasure -Learning.IT.step -Learning.IT.hist -Learning.IT.filtration -Learning.IT.adapted_step -Learning.IT.adapted_hist -ProbabilityTheory.Kernel.condDistrib_trajMeasure -Learning.IsAlgEnvSeq.hasLaw_step_zero -Learning.IT.action -Learning.IT.feedback -Learning.IT.adapted_action -Learning.IT.adapted_feedback -Learning.IT.condDistrib_action -Learning.IT.condDistrib_feedback -Learning.IT.hasLaw_action_zero -Learning.IT.condDistrib_feedback_zero -Learning.IT.isAlgEnvSeq_trajMeasure -Learning.pullCount -Learning.pullCount_zero -Learning.pullCount_mono -Learning.pullCount_add_one -Learning.pullCount_le -Learning.pullCount_congr -Learning.isPredictable_pullCount -Learning.stepsUntil -Learning.stepsUntil_zero_of_ne -Learning.stepsUntil_zero_of_eq -Learning.stepsUntil_pullCount_le -Learning.stepsUntil_pullCount_eq -Learning.action_stepsUntil -Learning.pullCount_stepsUntil_add_one -Learning.pullCount_stepsUntil -Learning.isStoppingTime_stepsUntil -Learning.rewardByCount -Learning.rewardByCount_pullCount_add_one_eq_reward -Learning.sumRewards -Learning.empMean -Learning.IsAlgEnvSeq.isPredictable_sumRewards -Learning.IsAlgEnvSeq.isPredictable_empMean -Learning.sum_rewardByCount_eq_sumRewards -Bandits.ArrayModel.probSpace -Bandits.ArrayModel.arrayMeasure -Bandits.ArrayModel.algFunction -Bandits.ArrayModel.initAlgFunction -Bandits.ArrayModel.hist -Bandits.ArrayModel.action -Bandits.ArrayModel.reward -Bandits.ArrayModel.measurable_hist -Bandits.ArrayModel.measurable_action -Bandits.ArrayModel.measurable_reward -Bandits.ArrayModel.hist_congr -Bandits.ArrayModel.stepsUntil_congr -Bandits.ArrayModel.truePast -Bandits.ArrayModel.measurable_hist_comap -Bandits.ArrayModel.measurable_hist_truePast -Bandits.ArrayModel.measurable_action_add_one_truePast -Bandits.ArrayModel.measurable_pullCount_add_one_truePast -Bandits.ArrayModel.measurable_stepsUntil -Bandits.ArrayModel.measurable_pullCount_action_add_one_hist -Bandits.ArrayModel.indepFun_fst_add_one_aux -Bandits.ArrayModel.indepFun_fst_add_one_hist -Bandits.ArrayModel.indepFun_snd_apply_aux -Bandits.ArrayModel.indepFun_snd_apply_pullCount_action -Bandits.ArrayModel.indepFun_snd_hist_cond -Bandits.ArrayModel.hasLaw_action_zero -Bandits.ArrayModel.hasCondDistrib_reward_zero -Bandits.ArrayModel.hasCondDistrib_action -Bandits.ArrayModel.hasCondDistrib_reward_pullCount_action -Bandits.ArrayModel.hasCondDistrib_reward_hist_action_pullCount -Bandits.ArrayModel.condIndepFun_reward_hist -Bandits.ArrayModel.hasCondDistrib_reward -Bandits.ArrayModel.isAlgEnvSeq_arrayMeasure -Learning.measurable_comap_indicator_stepsUntil_eq -Bandits.condIndepFun_reward_stepsUntil_action -Bandits.reward_cond_stepsUntil -ProbabilityTheory.condDistrib_ae_eq_cond -Bandits.condDistrib_rewardByCount_stepsUntil -Bandits.hasLaw_rewardByCount -Bandits.regret -Bandits.gap -Learning.sum_pullCount_mul -Bandits.regret_eq_sum_pullCount_mul_gap -Bandits.integral_regret_eq_sum_gap_mul_integral_pullCount -ProbabilityTheory.HasSubgaussianMGF -ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun -ProbabilityTheory.HasSubgaussianMGF.measure_ge_le -ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun -ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_sum_le' -Bandits.ArrayModel.identDistrib_sum_range_snd -Bandits.ArrayModel.prob_pullCount_prod_sumRewards_mem_le -Bandits.prob_pullCount_prod_sumRewards_mem_le -Bandits.ArrayModel.prob_sumRewards_le_sumRewards_le -Bandits.probReal_sumRewards_le_sumRewards_le -Bandits.probReal_sum_le_sum_streamMeasure -Bandits.prob_sum_le_sqrt_log -Bandits.prob_sum_ge_sqrt_log -Learning.RoundRobin.nextAction -Learning.roundRobinAlgorithm -Learning.RoundRobin.pullCount_mul -Bandits.ETC.nextArm -Bandits.etcAlgorithm -Bandits.ETC.isAlgEnvSeqUntil_roundRobinAlgorithm -Bandits.ETC.pullCount_of_ge -Bandits.ETC.sumRewards_bestArm_le_of_arm_mul_eq -Bandits.ETC.prob_arm_mul_eq_le -Bandits.ETC.regret_le -Bandits.UCB.nextArm -Bandits.ucbAlgorithm -Bandits.UCB.isAlgEnvSeqUntil_roundRobinAlgorithm -Bandits.UCB.ucbIndex_le_ucbIndex_arm -Bandits.UCB.gap_arm_le_two_mul_ucbWidth -Bandits.UCB.pullCount_arm_le -Bandits.UCB.prob_ucbIndex_le -Bandits.UCB.prob_ucbIndex_ge -Bandits.UCB.pullCount_le_add_three -Bandits.UCB.pullCount_le_add_three_ae -Bandits.UCB.some_sum_eq_zero -Bandits.UCB.expectation_pullCount_le -Bandits.UCB.regret_le -ProbabilityTheory.CondIndepFun.prod_right -ProbabilityTheory.iIndepFun_nat_iff_forall_indepFun diff --git a/blueprint/src/appendix/conditional_independence.tex b/blueprint/src/appendix/conditional_independence.tex deleted file mode 100644 index 14a678bd..00000000 --- a/blueprint/src/appendix/conditional_independence.tex +++ /dev/null @@ -1,45 +0,0 @@ -\chapter{Conditional independence} - - -\begin{lemma}\label{lem:CondIndepFun.prod_right} - \leanok - \lean{ProbabilityTheory.CondIndepFun.prod_right} -If $X \ind Y \mid Z$, then $X \ind (Y, Z) \mid Z$. -\end{lemma} - -\begin{proof}\leanok - -\end{proof} - - -\begin{lemma}[Contraction]\label{lem:indepFun_contraction} -If $X \ind Y \mid Z$ and $X \ind Z$, then $X \ind (Y, Z)$. -\end{lemma} - -\begin{proof} -It suffices to show that $\mathcal{L}(X \mid Y, Z) = \mathcal{L}(X)$. -By conditional independence, $\mathcal{L}(X \mid Y, Z) = \mathcal{L}(X \mid Z)$. -By independence, $\mathcal{L}(X \mid Z) = \mathcal{L}(X)$. -\end{proof} - - -\begin{lemma}\label{lem:condIndepFun_contraction} -If $X \ind Y \mid Z, W$ and $X \ind Z \mid W$, then $X \ind (Y, Z) \mid W$. -\end{lemma} - -\begin{proof} -It suffices to show that $\mathcal{L}(X \mid Y, Z, W) = \mathcal{L}(X \mid W)$. -By the first hypothesis, $\mathcal{L}(X \mid Y, Z, W) = \mathcal{L}(X \mid Z, W)$. -By the second hypothesis, $\mathcal{L}(X \mid Z, W) = \mathcal{L}(X \mid W)$. -\end{proof} - - -\begin{lemma}\label{lem:iIndepFun_nat_iff_forall_indepFun} - \leanok - \lean{ProbabilityTheory.iIndepFun_nat_iff_forall_indepFun} -A family of random variables $(X_i)_{i \in \mathbb{N}}$ is independent if and only if for all $n \in \mathbb{N}$, $X_{n+1}$ is independent of $(X_0, \ldots, X_n)$. -\end{lemma} - -\begin{proof}\leanok - -\end{proof} diff --git a/blueprint/src/biblio.bib b/blueprint/src/biblio.bib deleted file mode 100644 index f6e1818e..00000000 --- a/blueprint/src/biblio.bib +++ /dev/null @@ -1,278 +0,0 @@ -@book{bogachev2007measure, - title = {Measure theory}, - author = {V. I. Bogachev and M. A. S. Ruas}, - volume = {1}, - year = {2007}, - publisher = {Springer} -} - -@book{Billingsley1995, - author = {Billingsley, P.}, - title = {{Probability and Measure. 3rd ed.}}, - publisher = {{Wiley Series in - Probability and Statistics}}, - year = 1995, - keywords = {{measure theory; probability theory; stochastic processes}} -} - -@inproceedings{ying2023formalization, - title = {A Formalization of {D}oob’s Martingale Convergence Theorems in mathlib}, - author = {K. Ying and R. Degenne}, - booktitle = {Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs}, - pages = {334--347}, - year = {2023} -} - -@article{lean, - author = {Ebner, Gabriel and Ullrich, Sebastian and Roesch, Jared and Avigad, Jeremy and de Moura, Leonardo}, - title = {A {M}etaprogramming {F}ramework for {F}ormal {V}erification}, - year = {2017}, - issue_date = {September 2017}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - volume = {1}, - number = {ICFP}, - url = {https://doi.org/10.1145/3110278}, - doi = {10.1145/3110278}, - abstract = {We describe the metaprogramming framework currently used in Lean, an interactive theorem prover based on dependent type theory. This framework extends Lean's object language with an API to some of Lean's internal structures and procedures, and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our implementation is performant, and that it provides a convenient and flexible way of writing not only small-scale interactive tactics, but also more substantial kinds of automation.}, - journal = {Proc. ACM Program. Lang.}, - month = {aug}, - articleno = {34}, - numpages = {29}, - keywords = {tactic language, theorem proving, dependent type theory, metaprogramming} -} - -@inproceedings{moura2021lean, - title={The lean 4 theorem prover and programming language}, - author={Moura, Leonardo de and Ullrich, Sebastian}, - booktitle={International Conference on Automated Deduction}, - pages={625--635}, - year={2021}, - organization={Springer} -} - -@inproceedings{mathlib, - author = {{\ignorespaces The} {mathlib Community}}, - booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs}, - collection = {POPL '20}, - doi = {10.1145/3372885.3373824}, - month = jan, - year = {2020}, - title = {The {L}ean {M}athematical {L}ibrary}, - publisher = {Association for Computing Machinery}, - url = {https://doi.org/10.1145/3372885.3373824}, - doi = {10.1145/3372885.3373824}, - abstract = {This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. Among proof assistant libraries, it is distinguished by its dependently typed foundations, focus on classical mathematics, extensive hierarchy of structures, use of large- and small-scale automation, and distributed organization. We explain the architecture and design decisions of the library and the social organization that has led to its development.}, - booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs}, - pages = {367–381}, - numpages = {15}, - keywords = {formal library, Lean, formal proof, mathlib}, - location = {New Orleans, LA, USA}, - series = {CPP 2020} -} - -@book{kallenberg2021, - author = {Kallenberg, Olav}, - title = {Foundations of modern probability}, - series = {Probability Theory and Stochastic Modelling}, - volume = {99}, - publisher = {Springer Nature Switzerland}, - edition = {Third Edition}, - year = {2021}, - pages = {193}, - isbn = {978-3-030-61870-4; 978-3-030-61871-1}, - doi = {10.1007/978-3-030-61871-1}, - url = {https://doi.org/10.1007/978-3-030-61871-1} -} - -@article{Kolmogorov_Chentsov-AFP, - author = {Christian Pardillo-Laursen and Simon Foster}, - title = {The Kolmogorov-Chentsov theorem}, - journal = {Archive of Formal Proofs}, - month = {April}, - year = {2025}, - note = {\url{https://isa-afp.org/entries/Kolmogorov_Chentsov.html}, - Formal proof development}, - issn = {2150-914x} -} - -@misc{Immler2012, - author = {Immler, F.}, - title = {Generic - Construction of Probability Spaces for Paths of Stochastic Processes in Isabelle/HOL}, - journal = {Master’s Thesis in Informatik, TU Munich}, - year = {2012}, - url = {https://saloranta.de/immler/fabian/mastersthesis/thesis.pdf} -} - -@misc{defaultValues, - author = {Buzzard, Kevin}, - title = {Division by zero in type theory: A FAQ}, - year = {2020}, - url = {https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/}, - note = {Accessed: 2025-09-22} -} - -@article{holzl2017markov, - title = {Markov chains and Markov decision processes in Isabelle/HOL}, - author = {H{\"o}lzl, J.}, - journal = {Journal of Automated Reasoning}, - volume = {59}, - number = {3}, - pages = {345--387}, - year = {2017}, - publisher = {Springer} -} - -@software{Monticone_LeanProject_2025, - abstract = {A template for blueprint-driven formalization projects in Lean.}, - author = {Monticone, Pietro}, - institution = {University of Trento}, - keywords = {Lean4, Project Management, Formal Methods, Formal Verification, Theorem Proving, Interactive Theorem Proving, Proof Assistant, Mathematical Formalization, Formal Mathematics, Blueprint, Documentation, Template, Dependency Management, Continuous Integration, Automated Testing, Type Theory, Constructive Mathematics, Computer-Assisted Proof, Mathematical Software, Research Software Engineering}, - license = {Apache License 2.0}, - title = {LeanProject}, - year = {2025} -} - -@software{Anderson_Formalization_of_the_2023, -author = {Anderson, Aaron and Bakšys, Mantas and Bayer, Jonas and Collares, Mauricio and Degenne, Rémy and Dillies, Yaël and Eltschig, Ben and Gouëzel, Sébastien and Kytölä, Kalle and Lewis, Rob and Lez, Paul and Lorenzo, Luccioli and Macbeth, Heather and Massot, Patrick and Mellendijk, Arend and Miller, Kyle and Monticone, Pietro and Morrison, Kim and Nash, Oliver and Song, Utensil and Tao, Terence and van Doorn, Floris and Wilshaw, Sky and Wu, Lawrence}, -month = nov, -title = {{Formalization of the Polynomial Freiman-Ruzsa Conjecture of Marton}}, -url = {https://github.com/teorth/pfr}, -version = {0.1.0}, -year = {2023} -} - -@article{gowers2025conjecture, - title={On a conjecture of Marton}, - author={Gowers, William Timothy and Green, Ben and Manners, Freddie and Tao, Terence}, - journal={Annals of Mathematics}, - volume={201}, - number={2}, - pages={515--549}, - year={2025}, -} - -@article{faden1985existence, - title={The existence of regular conditional probabilities: necessary and sufficient conditions}, - author={Faden, Arnold M}, - journal={The Annals of Probability}, - pages={288--298}, - year={1985}, - publisher={JSTOR} -} - -@article{marion2025formalization, - title={A Formalization of the Ionescu-Tulcea Theorem in Mathlib}, - author={Marion, Etienne}, - journal={arXiv preprint arXiv:2506.18616}, - year={2025} -} - -@software{TestingLowerBounds, - author = {Luccioli, Lorenzo and Degenne, Rémy}, - title = {TestingLowerBounds}, - year = {2024}, - url = {https://github.com/RemyDegenne/testing-lower-bounds} -} - -@inproceedings{gouezel2022formalization, - title={A formalization of the change of variables formula for integrals in mathlib}, - author={Gou{\"e}zel, S{\'e}bastien}, - booktitle={International Conference on Intelligent Computer Mathematics}, - pages={3--18}, - year={2022}, - organization={Springer} -} - -@article{fritz2020synthetic, - title={A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics}, - author={Fritz, Tobias}, - journal={Advances in Mathematics}, - volume={370}, - pages={107239}, - year={2020}, - publisher={Elsevier} -} - -@article{forre2021transitional, - title={Transitional conditional independence}, - author={Forr{\'e}, Patrick}, - journal={arXiv preprint arXiv:2104.11547}, - year={2021} -} - -@book{vershynin2018high, - title={High-dimensional probability: An introduction with applications in data science}, - author={Vershynin, Roman}, - volume={47}, - year={2018}, - publisher={Cambridge university press} -} - -@article{hoeffding1963probability, - title={Probability inequalities for sums of bounded random variables}, - author={Hoeffding, Wassily}, - journal={Journal of the American statistical association}, - volume={58}, - number={301}, - pages={13--30}, - year={1963}, - publisher={Taylor \& Francis} -} - -@inproceedings{clerc2017pointless, - title={Pointless learning}, - author={Clerc, Florence and Danos, Vincent and Dahlqvist, Fredrik and Garnier, Ilias}, - booktitle={International conference on foundations of software science and computation structures}, - pages={355--369}, - year={2017}, - organization={Springer} -} - -@book{polyanskiy2025information, - title={Information theory: From coding to learning}, - author={Polyanskiy, Yury and Wu, Yihong}, - year={2025}, - publisher={Cambridge university press} -} - -@article{vakar2018s, - title={On s-finite measures and kernels}, - author={V{\'a}k{\'a}r, Matthijs and Ong, Luke}, - journal={arXiv preprint arXiv:1810.01837}, - year={2018} -} - -@article{affeldt2025semantics, - title={Semantics of Probabilistic Programs using s-Finite Kernels in Dependent Type Theory}, - author={Affeldt, Reynald and Cohen, Cyril and Saito, Ayumu}, - journal={ACM Transactions on Probabilistic Machine Learning}, - year={2025}, - publisher={ACM New York, NY} -} - -@article{staton2020probabilistic, - title={Probabilistic programs as measures}, - author={Staton, Sam}, - journal={Foundations of Probabilistic Programming}, - pages={43}, - year={2020}, - publisher={Cambridge University Press} -} - -@inproceedings{hirata2023semantic, - title={Semantic foundations of higher-order probabilistic programs in Isabelle/HOL}, - author={Hirata, Michikazu and Minamide, Yasuhiko and Sato, Tetsuya}, - booktitle={14th International Conference on Interactive Theorem Proving (ITP 2023)}, - pages={18--1}, - year={2023}, - organization={Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik} -} - -@book{lattimore2020bandit, - title={Bandit algorithms}, - author={Lattimore, Tor and Szepesv{\'a}ri, Csaba}, - year={2020}, - publisher={Cambridge University Press} -} diff --git a/blueprint/src/blueprint.sty b/blueprint/src/blueprint.sty deleted file mode 100644 index 1353f398..00000000 --- a/blueprint/src/blueprint.sty +++ /dev/null @@ -1,2 +0,0 @@ -\DeclareOption*{} -\ProcessOptions \ No newline at end of file diff --git a/blueprint/src/chapters/algorithm.tex b/blueprint/src/chapters/algorithm.tex deleted file mode 100644 index ccae536c..00000000 --- a/blueprint/src/chapters/algorithm.tex +++ /dev/null @@ -1,601 +0,0 @@ -\chapter{Iterative stochastic algorithms} - - -Warning: all times start at zero. - -TODO: notations - -All measurable spaces are assumed to be standard Borel. - - -\begin{definition}[Algorithm]\label{def:algorithm} - \leanok - \lean{Learning.Algorithm} -A sequential, stochastic algorithm with actions in a measurable space $\mathcal{A}$ and observations in a measurable space $\mathcal{R}$ is described by the following data: -\begin{itemize} - \item for all $t \in \mathbb{N}$, a policy $\pi_t : (\mathcal{A} \times \mathcal{R})^{t+1} \rightsquigarrow \mathcal{A}$, a Markov kernel which gives the distribution of the action of the algorithm at time $t+1$ given the history of previous actions and observations, - \item $P_0 \in \mathcal{P}(\mathcal{A})$, a probability measure that gives the distribution of the first action. -\end{itemize} -\end{definition} - -After the algorithm takes an action, the environment generates an observation according to a Markov kernel $\nu_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times \mathcal{A} \rightsquigarrow \mathcal{R}$. - - -\begin{definition}[Environment]\label{def:environment} - \leanok - \lean{Learning.Environment} -An environment with which an algorithm interacts is described by the following data: -\begin{itemize} - \item for all $t \in \mathbb{N}$, a feedback $\nu_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times \mathcal{A} \rightsquigarrow \mathcal{R}$, a Markov kernel which gives the distribution of the observation at time $t+1$ given the history of previous pulls and observations, and the action of the algorithm at time $t+1$, - \item $\nu'_0 \in \mathcal{A} \rightsquigarrow \mathcal{R}$, a Markov kernel that gives the distribution of the first observation given the first action. -\end{itemize} -\end{definition} - - -\begin{definition}[Deterministic algorithm]\label{def:detAlgorithm} - \uses{def:algorithm} - \leanok - \lean{Learning.detAlgorithm} -An algorithm is deterministic if its initial probability measure $P_0$ is a Dirac measure and if all its policies $\pi_t$ are deterministic kernels. -\end{definition} - - -\begin{definition}[Stationary environment]\label{def:stationaryEnv} - \uses{def:environment} - \leanok - \lean{Learning.stationaryEnv} -An environment is stationary if there exists a Markov kernel $\nu : \mathcal{A} \rightsquigarrow \mathcal{R}$ such that $\nu'_0 = \nu$ and for all $t \in \mathbb{N}$, for all $h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}$, for all $a \in \mathcal{A}$, $\nu_t(h_t, a) = \nu(a)$. -\end{definition} - -TODO: possibly change the ``stationary'' name. - - -Let's detail four examples of interactions between an algorithm and an environment. -\begin{enumerate} - \item \textbf{First order optimization}. The objective of the algorithm is to find the minimum of a function $f : \mathbb{R}^d \to \mathbb{R}$. - The action space is $\mathcal{A} = \mathbb{R}^d$ (a point on which the function will be queried) and the observation space is $\mathcal{R} = \mathbb{R} \times \mathbb{R}^d$. - The environment is described by a function $g : \mathbb{R}^d \to \mathbb{R} \times \mathbb{R}^d$ such that for all $x \in \mathbb{R}^d$, $g(x) = (f(x), \nabla f(x))$. That is, the kernel $\nu_t$ is deterministic and depends only on the action: it is given by $\nu_t(h_t, x) = \delta_{g(x)}$ (the Dirac measure at $g(x)$). - An example of algorithm is gradient descent with fixed step size $\eta > 0$: this is a deterministic algorithm defined by $P_0 = \delta_{x_0}$ for some initial point $x_0 \in \mathbb{R}^d$ and for all $t \in \mathbb{N}$, $\pi_t(h_t) = \delta_{x_{t+1}}$ where $x_{t+1} = x_t - \eta \nabla g_2(x_t)$. - - \item \textbf{Stochastic bandits}. The action space is $\mathcal{A} = [K]$ for some $K \in \mathbb{N}$ (the set of arms) and the observation space is $\mathcal{R} = \mathbb{R}$ (the reward obtained after pulling an arm). - The kernel $\nu_t$ is stationary and depends only on the action: there are probability distributions $(P_a)_{a \in [K]}$ such that for all $t \in \mathbb{N}$, for all $h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}$, for all $a \in \mathcal{A}$, $\nu_t(h_t, a) = P_a$. - - \item \textbf{Adversarial bandits}. The action space is $\mathcal{A} = [K]$ for some $K \in \mathbb{N}$ (the set of arms) and the observation space is $\mathcal{R} = \mathbb{R}$ (the reward obtained after pulling an arm). - The reward kernels are usually taken to be deterministic and in an \emph{oblivious} adversarial bandit they depend only on the time step: there is a sequence of vectors $(r_t)_{t \in \mathbb{N}}$ in $[0,1]^K$ such that for all $t \in \mathbb{N}$, for all $h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}$, for all $a \in \mathcal{A}$, $\nu_t(h_t, a) = \delta_{r_{t,a}}$ (the Dirac measure at $r_{t,a}$). - - \item \textbf{Reinforcement learning in Markov decision processes}. - TODO: main feature is that $\mathcal{R} = \mathcal{S} \times \mathbb{R}$ where $\mathcal{S}$ is the state space, and the kernel $\nu_t$ depends on the last state only. -\end{enumerate} - - -We will want to make global probabilistic statements about the whole sequence of actions and observations. -For example, we may want to prove that an optimization algorithm converges to the minimum of a function almost surely. -For such a statement to make sense, we need a probability space on which the whole sequence of actions and observations is defined as a random variable. - -We denote by $P(X \mid Y)$ the conditional distribution of a random variable $X$ given another random variable $Y$ under a probability measure $P$. -When we write that $P(X \mid Y) = \kappa$, or that $X$ has conditional distribution $\kappa$ given $Y$, the equality should be understood as holding $Y_* P$-almost surely. - - -\begin{remark}[Lean remark: \texttt{HasCondDistrib}] -In the Lean implementation, we define a predicate to state those almost sure equalities of conditional distributions: \texttt{HasCondDistrib X Y k P} states that under the probability measure $P$, the random variable $X$ has conditional distribution $k$ given the random variable $Y$ (almost surely with respect to the law of $X$). -For convenience, the predicate also records that both random variables are almost everywhere measurable. -\end{remark} - - -\begin{definition}[Algorithm-environment interaction]\label{def:IsAlgEnvSeq} - \uses{def:environment,def:algorithm,def:history} - \leanok - \lean{Learning.IsAlgEnvSeq} -Let $\mathfrak{A}$ be an algorithm as in Definition~\ref{def:algorithm} and $\mathfrak{E}$ be an environment as in Definition~\ref{def:environment}. -A probability space $(\Omega, P)$ and two sequences of random variables $A : \mathbb{N} \to \Omega \to \mathcal{A}$ and $R : \mathbb{N} \to \Omega \to \mathcal{R}$ form an algorithm-environment interaction for $\mathfrak{A}$ and $\mathfrak{E}$ if the following conditions hold: -\begin{enumerate} - \item The law of $A_0$ is $P_0$. - \item $P \left( R_0 \mid A_0 \right) = \nu'_0$. - \item For all $t \in \mathbb{N}$, $P\left(A_{t+1} \mid A_0, R_0, \ldots, A_t, R_t \right) = \pi_t$. - \item For all $t \in \mathbb{N}$, $P\left(R_{t+1} \mid A_0, R_0, \ldots, A_t, R_t, A_{t+1}\right) = \nu_t$. -\end{enumerate} -\end{definition} - - -\begin{definition}[History]\label{def:history} - \leanok - \lean{Learning.IsAlgEnvSeq.hist, Learning.IsAlgEnvSeq.step} -For two sequences of random variables $A : \mathbb{N} \to \Omega \to \mathcal{A}$ and $R : \mathbb{N} \to \Omega \to \mathcal{R}$ (actions and observations), we call step of the interaction at time $t$ the random variable $X_t : \Omega \to \mathcal{A} \times \mathcal{R}$ defined by $X_t(\omega) = (A_t(\omega), R_t(\omega))$. -We call history up to time $t$ the random variable $H_t : \Omega \to (\mathcal{A} \times \mathcal{R})^{t+1}$ defined by $H_t(\omega) = (X_0(\omega), \ldots, X_t(\omega))$. -\end{definition} - - -\begin{lemma}\label{lem:law_step} - \uses{def:environment,def:IsAlgEnvSeq,def:algorithm,def:history} - \leanok - \lean{Learning.IsAlgEnvSeq.hasLaw_step_zero, Learning.IsAlgEnvSeq.hasCondDistrib_step} -In an algorithm-environment interaction $(A, R, P)$ as in Definition~\ref{def:IsAlgEnvSeq}, -\begin{itemize} - \item the law of the initial step $X_0$ is $P_0 \otimes \nu'_0$, - \item for all $t \in \mathbb{N}$, $P \left( X_{t+1} \mid H_t \right) = \pi_t \otimes \nu_t$. -\end{itemize} -\end{lemma} - -\begin{proof}\leanok -Immediate from the properties of an algorithm-environment interaction. -\end{proof} - - -\begin{definition}\label{def:IsAlgEnvSeq.filtration} - \uses{def:history} - \leanok - \lean{Learning.IsAlgEnvSeq.filtration, Learning.IsAlgEnvSeq.filtrationAction} -For an algorithm-environment interaction $(A, R, P)$ as in Definition~\ref{def:IsAlgEnvSeq}, we denote by $\mathcal{F}_t$ the sigma-algebra generated by the history up to time $t$: $\mathcal{F}_t = \sigma(H_t)$. -We denote by $\mathcal{F}^A_t$ the sigma-algebra generated by the history up to time $t-1$ and the action at time $t$: $\mathcal{F}^A_t = \sigma(H_{t-1}, A_t)$. -\end{definition} - - -\begin{lemma}\label{lem:IsAlgEnvSeq.adapted} - \uses{def:IsAlgEnvSeq.filtration,def:history} - \leanok - \lean{Learning.IsAlgEnvSeq.adapted_step, Learning.IsAlgEnvSeq.adapted_hist, Learning.IsAlgEnvSeq.adapted_action, Learning.IsAlgEnvSeq.adapted_feedback} -The history, step, action and observation processes are adapted to the filtration $(\mathcal{F}_t)_{t \in \mathbb{N}}$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:history,def:IsAlgEnvSeq.filtration} -By definition of the filtration. -\end{proof} - - -\begin{theorem}[\cite{lattimore2020bandit}, Proposition 4.8]\label{thm:isAlgEnvSeq_unique} - \uses{def:environment,def:IsAlgEnvSeq,def:algorithm} - \leanok - \lean{Learning.isAlgEnvSeq_unique} -If $(A, R, P)$ and $(A', R', P')$ are two algorithm-environment interactions for the same algorithm $\mathfrak{A}$ and environment $\mathfrak{E}$, then the joint distributions of the sequences of actions and observations are equal: the law of $(A_i, R_i)_{i \in \mathbb{N}}$ under $P$ is equal to the law of $(A'_i, R'_i)_{i \in \mathbb{N}}$ under $P'$. -\end{theorem} - -\begin{proof}\leanok - \uses{thm:ionescu-tulcea,lem:law_step,def:trajMeasure} - -\end{proof} - - - -\section{Stationary environment} - -Recall that in a stationary environment, there exists a Markov kernel $\nu : \mathcal{A} \rightsquigarrow \mathcal{R}$ such that $\nu'_0 = \nu$ and for all $t \in \mathbb{N}$, for all $h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}$, for all $a \in \mathcal{A}$, $\nu_t(h_t, a) = \nu(a)$. - -Let $(A, R, P)$ be an algorithm-environment interaction in a stationary environment with kernel $\nu$. - -\begin{lemma}\label{lem:condDistrib_reward_stationaryEnv} - \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:algorithm} - \leanok - \lean{Learning.IsAlgEnvSeq.condDistrib_feedback_stationaryEnv} -In a stationary environment, for any $t \in \mathbb{N}$, $P\left(R_t \mid A_t\right) = \nu$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:environment,lem:law_step,def:history} - -\end{proof} - - -\begin{lemma}\label{lem:condIndepFun_reward_hist_action} - \uses{def:stationaryEnv,def:environment,def:IsAlgEnvSeq,def:algorithm,def:history} - \leanok - \lean{Learning.IsAlgEnvSeq.condIndepFun_feedback_hist_action} -In a stationary environment, for any $t \in \mathbb{N}$, the reward $R_{t+1}$ is conditionally independent of the history $H_t$ given the action $A_{t+1}$ (more succinctly, $R_{t+1} \ind H_t \mid A_{t+1}$). -\end{lemma} - -\begin{proof}\leanok - -\end{proof} - - - -\section{Probability space: Ionescu-Tulcea theorem} - -In Theorem~\ref{thm:isAlgEnvSeq_unique}, we saw that the distribution of the sequence of actions and observations in a suitable probability space is uniquely determined by the algorithm and the environment. -We now show that such a probability space actually exists: for any algorithm and environment, we build an algorithm-environment interaction as in Definition~\ref{def:IsAlgEnvSeq}. - - - -\subsection{Ionescu-Tulcea theorem} - -If we group together the policy of the algorithm and the kernel of the environment at each time step, we get a sequence of Markov kernels $(\kappa_t)_{t \in \mathbb{N}}$, with $\kappa_t : (\mathcal{A} \times \mathcal{R})^{t+1} \rightsquigarrow (\mathcal{A} \times \mathcal{R})$. - - -We now abstract that situation and consider a sequence of measurable spaces $(\Omega_t)_{t \in \mathbb{N}}$, a probability measure $\mu$ on $\Omega_0$ and a sequence of Markov kernels $\kappa_t : \prod_{s=0}^t \Omega_s \rightsquigarrow \Omega_{t+1}$. -The Ionescu-Tulcea theorem builds a probability space from the sequence of kernels and the initial measure. - - -\begin{theorem}[Ionescu-Tulcea]\label{thm:ionescu-tulcea} - \mathlibok - \lean{ProbabilityTheory.Kernel.traj} -Let $(\Omega_t)_{t \in \mathbb{N}}$ be a family of measurable spaces. Let $(\kappa_t)_{t \in \mathbb{N}}$ be a family of Markov kernels such that for any $t$, $\kappa_t$ is a kernel from $\prod_{i=0}^t \Omega_{i}$ to $\Omega_{t+1}$. -Then there exists a unique Markov kernel $\xi : \Omega_0 \rightsquigarrow \prod_{i = 1}^{\infty} \Omega_{i}$ such that for any $n \ge 1$, -$\pi_{[1,n]*} \xi = \kappa_0 \otimes \ldots \otimes \kappa_{n-1}$. -Here $\pi_{[1,n]} : \prod_{i=1}^{\infty} \Omega_i \to \prod_{i=1}^n \Omega_i$ is the projection on the first $n$ coordinates. -\end{theorem} - -\begin{proof}\leanok -\end{proof} - -The Ionescu-Tulcea theorem in Mathlib \cite{marion2025formalization} actually generates kernels $\xi_t : \prod_{s=0}^t \Omega_s \rightsquigarrow \prod_{s=0}^{\infty} \Omega_s$ for any $t$, with the property that the kernels are the identity on the first $t+1$ coordinates. - -\begin{definition}[Trajectory measure]\label{def:trajMeasure} - \uses{thm:ionescu-tulcea} - \leanok - \lean{ProbabilityTheory.Kernel.trajMeasure} -For $\mu \in \mathcal{P}(\Omega_0)$, we call trajectory measure the probability measure $\xi_0 \circ \mu$ on $\Omega_{\mathcal{T}} := \prod_{i=0}^{\infty} \Omega_i$. -We denote it by $P_{\mathcal{T}}$. -The $\mathcal{T}$ subscript stands for ``trajectory''. -\end{definition} - - -\begin{definition}[Step and history]\label{def:IT.history} - \leanok - \lean{Learning.IT.step, Learning.IT.hist} -For $t \in \mathbb{N}$, we denote by $X_t \in \Omega_t$ the random variable describing the time step $t$, and by $H_t \in \prod_{s=0}^t \Omega_s$ the history up to time $t$. -Formally, these are measurable functions on $\Omega_{\mathcal{T}}$, defined by $X_t(\omega) = \omega_t$ and $H_t(\omega) = (\omega_1, \ldots, \omega_t)$. -\end{definition} - -Note: $(X_t)_{t \in \mathbb{N}}$ is the canonical process on $\Omega_{\mathcal{T}}$. $H_t$ is equal to $\pi_{[0,t]}$. - - -\begin{definition}[Filtration]\label{def:IT.filtration} - \uses{def:IT.history} - \leanok - \lean{Learning.IT.filtration} -For $t \in \mathbb{N}$, we denote by $\mathcal{F}_t$ the sigma-algebra generated by the history up to time $t$: $\mathcal{F}_t = \sigma(H_t)$. -The family $(\mathcal{F}_t)_{t \in \mathbb{N}}$ is a filtration on $\Omega_{\mathcal{T}}$. -\end{definition} - -$(\mathcal{F}_t)_{t \in \mathbb{N}}$ is the canonical filtration on $\Omega_{\mathcal{T}}$, and is the natural filtration for the canonical process $(X_t)_{t \in \mathbb{N}}$. - - -\begin{lemma}\label{lem:IT.adapted_history} - \uses{def:IT.history, def:IT.filtration} - \leanok - \lean{Learning.IT.adapted_step, Learning.IT.adapted_hist} -The random variables $X_t$ and $H_t$ are $\mathcal{F}_t$-measurable. -Said differently, the processes $(X_t)_{t \in \mathbb{N}}$ and $(H_t)_{t \in \mathbb{N}}$ are adapted to the filtration $(\mathcal{F}_t)_{t \in \mathbb{N}}$. -\end{lemma} - -\begin{proof}\leanok - -\end{proof} - - -\begin{lemma}\label{lem:IT.condDistrib_X_add_one} - \uses{def:IT.history, thm:ionescu-tulcea, def:trajMeasure} - \leanok - \lean{ProbabilityTheory.Kernel.condDistrib_trajMeasure} -For any $t \in \mathbb{N}$, $P_{\mathcal{T}}\left(X_{t+1} \mid H_t\right) = \kappa_t$. -\end{lemma} - -\begin{proof}\leanok -This is proved through the defining property of the conditional distribution: it is the almost surely unique Markov kernel $\eta$ such that $((H_t)_* P_{\mathcal{T}}) \otimes \eta = (H_t, X_{t+1})_*P_{\mathcal{T}}$. - -TODO: complete proof. -\end{proof} - - -\begin{lemma}\label{lem:IT.law_X_zero} - \uses{def:IT.history, def:trajMeasure} - \leanok - \lean{Learning.IsAlgEnvSeq.hasLaw_step_zero} -The law of $X_0$ under $P_{\mathcal{T}}$ is $\mu$. -\end{lemma} - -\begin{proof}\leanok - -\end{proof} - - - - -\subsection{Case of an algorithm-environment interaction} - -We now go back to the setting of an algorithm interacting with an environment and suppose that $\Omega_t = \mathcal{A} \times \mathcal{R}$ for some measurable spaces $\mathcal{A}$ and $\mathcal{R}$, and that for all $t \in \mathbb{N}$, $\kappa_t = \pi_t \otimes \nu_t$ for policy kernels $\pi_t : (\mathcal{A} \times \mathcal{R})^{t+1} \rightsquigarrow \mathcal{A}$ and feedback kernels $\nu_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times \mathcal{A} \rightsquigarrow \mathcal{R}$. -Likewise, $\mu = P_0 \otimes \nu'_0$ for a probability measure $P_0$ on $\mathcal{A}$ and a Markov kernel $\nu'_0 : \mathcal{A} \rightsquigarrow \mathcal{R}$. -The step random variable $X_t$ takes values in $\mathcal{A} \times \mathcal{R}$. - -\begin{definition}\label{def:IT.actionReward} - \uses{def:IT.history} - \leanok - \lean{Learning.IT.action, Learning.IT.feedback} -We write $A_t$ and $R_t$ for the projections of $X_t$ on $\mathcal{A}$ and $\mathcal{R}$ respectively. -$A_t$ is the action taken at time $t$ and $R_t$ is the reward received at time $t$. -Formally, $A_t(\omega) = \omega_{t,1}$ and $R_t(\omega) = \omega_{t,2}$ for $\omega = \prod_{t=0}^{+\infty}(\omega_{t,1}, \omega_{t,2}) \in \Omega_{\mathcal{T}} = \prod_{t=0}^{+\infty} \mathcal{A} \times \mathcal{R}$. -\end{definition} - - -\begin{lemma}\label{lem:IT.adapted_action_reward} - \uses{def:IT.actionReward, def:IT.filtration} - \leanok - \lean{Learning.IT.adapted_action, Learning.IT.adapted_feedback} -The random variables $A_t$ and $R_t$ are $\mathcal{F}_t$-measurable. -Said differently, the processes $(A_t)_{t \in \mathbb{N}}$ and $(R_t)_{t \in \mathbb{N}}$ are adapted to the filtration $(\mathcal{F}_t)_{t \in \mathbb{N}}$. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:IT.adapted_history} - -\end{proof} - - -We need to check that the random variables $A_t$ and $R_t$ have the expected conditional distributions. - -\begin{lemma}\label{lem:IT.condDistrib_A_add_one} - \uses{def:environment,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure,def:IT.history} - \leanok - \lean{Learning.IT.condDistrib_action} -For any $t \in \mathbb{N}$, $P_{\mathcal{T}}\left(A_{t+1} \mid H_t\right) = \pi_t$. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:IT.condDistrib_X_add_one,def:IT.history} -By Lemma~\ref{lem:IT.condDistrib_X_add_one}, $P_{\mathcal{T}}\left(X_{t+1} \mid H_t\right) = \kappa_t = \pi_t \otimes \nu_t$. -Since $A_{t+1}$ is the projection of $X_{t+1}$ on $\mathcal{A}$, $P_{\mathcal{T}}\left(A_{t+1} \mid H_t\right)$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to the projection of $\kappa_t$ on $\mathcal{A}$, which is $\pi_t$. -\end{proof} - - -\begin{lemma}\label{lem:IT.condDistrib_R_add_one} - \uses{def:environment,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure,def:IT.history} - \leanok - \lean{Learning.IT.condDistrib_feedback} -For any $t \in \mathbb{N}$, $P_{\mathcal{T}}\left(R_{t+1} \mid H_t, A_{t+1}\right) = \nu_t$. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:IT.condDistrib_X_add_one,def:IT.history,lem:IT.condDistrib_A_add_one} -It suffices to show that $((H_t, A_{t+1})_* P_{\mathcal{T}}) \otimes \nu_t = (H_t, A_{t+1}, R_{t+1})_* P_{\mathcal{T}} = (H_t, X_{t+1})_* P_{\mathcal{T}}$. -By Lemma~\ref{lem:IT.condDistrib_X_add_one}, $P_{\mathcal{T}}\left(X_{t+1} \mid H_t\right) = \pi_t \otimes \nu_t$. -Thus $((H_t)_* P_{\mathcal{T}}) \otimes (\pi_t \otimes \nu_t) = (H_t, X_{t+1})_* P_{\mathcal{T}}$. - -We thus have to prove that $((H_t)_* P_{\mathcal{T}}) \otimes (\pi_t \otimes \nu_t) = ((H_t, A_{t+1})_* P_{\mathcal{T}}) \otimes \nu_t$. - -By Lemma~\ref{lem:IT.condDistrib_A_add_one}, $(H_t, A_{t+1})_* P_{\mathcal{T}} = (H_t)_* P_{\mathcal{T}} \otimes \pi_t$, and replacing this in the right-hand side gives the left-hand side (using associativity of the composition-product). -\end{proof} - - -\begin{lemma}\label{lem:IT.law_A_zero} - \uses{def:environment,def:algorithm,def:IT.actionReward,def:trajMeasure} - \leanok - \lean{Learning.IT.hasLaw_action_zero} -The law of $A_0$ under $P_{\mathcal{T}}$ is $P_0$. -\end{lemma} - -\begin{proof}\leanok - \uses{thm:ionescu-tulcea,def:IT.history,lem:IT.law_X_zero} -$X_0$ has law $\mu = P_0 \otimes \nu'_0$. $A_0$ is the projection of $X_0$ on the first space $\mathcal{A}$ and $\nu_0'$ is Markov, so $A_0$ has law $P_0$. -\end{proof} - - -\begin{lemma}\label{lem:IT.condDistrib_R_zero} - \uses{def:environment,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure} - \leanok - \lean{Learning.IT.condDistrib_feedback_zero} -$P_{\mathcal{T}}\left(R_0 \mid A_0\right) = \nu'_0$. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:IT.law_X_zero,lem:IT.law_A_zero,def:IT.history} -To prove almost sure equality, it is enough to prove that $(A_{0*} P_{\mathcal{T}}) \otimes P_{\mathcal{T}}\left(R_0 \mid A_0\right) = (A_{0*} P_{\mathcal{T}}) \otimes \nu'_0$. -By definition of the conditional distribution, we have $(A_{0*} P_{\mathcal{T}}) \otimes P_{\mathcal{T}}\left(R_0 \mid A_0\right) = (A_0, R_0)_* P_{\mathcal{T}} = X_{0*} P_{\mathcal{T}}$. -By Lemma~\ref{lem:IT.law_X_zero}, $X_{0*} P_{\mathcal{T}} = \mu = P_0 \otimes \nu'_0$. -By Lemma~\ref{lem:IT.law_A_zero}, $A_{0*} P_{\mathcal{T}} = P_0$. -Thus the two sides are equal. -\end{proof} - - -\begin{theorem}\label{thm:isAlgEnvSeq_trajMeasure} - \uses{def:environment,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure} - \leanok - \lean{Learning.IT.isAlgEnvSeq_trajMeasure} -In the probability space $(\Omega_{\mathcal{T}}, P_{\mathcal{T}})$ constructed from an algorithm $\mathfrak{A}$ and an environment $\mathfrak{E}$ as above, the sequences of random variables $A : \mathbb{N} \to \Omega_{\mathcal{T}} \to \mathcal{A}$ and $R : \mathbb{N} \to \Omega_{\mathcal{T}} \to \mathcal{R}$ form an algorithm-environment interaction for $\mathfrak{A}$ and $\mathfrak{E}$. -\end{theorem} - -\begin{proof}\leanok - \uses{def:history,lem:IT.law_A_zero,lem:IT.condDistrib_R_zero,lem:IT.condDistrib_A_add_one,lem:IT.condDistrib_R_add_one} -The four conditions of Definition~\ref{def:IsAlgEnvSeq} are exactly the statements of Lemmas~\ref{lem:IT.law_A_zero}, \ref{lem:IT.condDistrib_R_zero}, \ref{lem:IT.condDistrib_A_add_one} and \ref{lem:IT.condDistrib_R_add_one}. -\end{proof} - - - -\section{Finitely many actions} - -When the number of actions is finite, it makes sense to count how many times each action was chosen up to a certain time. -We can also define the time step at which an action was chosen a certain number of times, and the value of the reward obtained when pulling an action for the $m$-th time. - -\begin{definition}[Pull counts]\label{def:pullCount} - \leanok - \lean{Learning.pullCount} -For an action $a \in \mathcal{A}$ and a time $t \in \mathbb{N}$, we denote by $N_{t,a}$ the number of times that action $a$ has been chosen before time $t$, that is $N_{t,a} = \sum_{s=0}^{t-1} \mathbb{I}\{A_s = a\}$. -\end{definition} - -Note that the sum goes up to $t-1$, so that $N_{t,a}$ counts the number of times action $a$ was chosen \emph{before} time $t$. - - -\begin{remark}[Building vs analyzing algorithms] -When we describe an algorithm, we give the data of the policies $\pi_t$, which are functions of the partial history up to time $t$, in $(\mathcal{A} \times \mathcal{R})^{t+1}$. -That means that any tool used to define a policy must be a function defined on $(\mathcal{A} \times \mathcal{R})^{t+1}$. -For example a definition of the empirical mean of an action must be a function $t : \mathbb{N} \to (\mathcal{A} \times \mathcal{R})^{t+1} \to \mathbb{R}$. - -When we analyze an algorithm, we work on the other hand on a probability space $(\Omega, P)$, in which $\Omega$ could be for example $(\mathcal{A} \times \mathcal{R})^{\mathbb{N}}$, the full history, which describes the whole sequence of actions and rewards. -As a stochastic process, the empirical mean of an action is a function $\mathbb{N} \to (\mathcal{A} \times \mathcal{R})^{\mathbb{N}} \to \mathbb{R}$. - -Thus there are two similar but still distinct types of objects: those defined on the partial history, which are used to build algorithms, and those defined on a generic probability space (the full history in the Ionescu-Tulcea construction), which are used to analyze algorithms. -\end{remark} - - -\begin{lemma}\label{lem:pullCount_basic} - \uses{def:pullCount, def:IT.actionReward} - \leanok - \lean{Learning.pullCount_zero, Learning.pullCount_mono, Learning.pullCount_add_one, Learning.pullCount_le, Learning.pullCount_congr} -We note the following basic properties of $N_{t,a}$: -\begin{itemize} - \item $N_{0,a} = 0$. - \item $N_{t,a}$ is non-decreasing in $t$. - \item $N_{t + 1, A_t} = N_{t, A_t} + 1$ and for $a \ne A_t$, $N_{t + 1, a} = N_{t, a}$. - \item $N_{t, a} \le t$. - \item If for all $s \le t$, $A_s(\omega) = A_s(\omega')$, then $N_{t+1, a}(\omega) = N_{t+1, a}(\omega')$. -\end{itemize} -\end{lemma} - -\begin{proof}\leanok - -\end{proof} - - -\begin{lemma}\label{lem:predictable_pullCount} - \uses{def:IsAlgEnvSeq.filtration, def:pullCount} - \leanok - \lean{Learning.isPredictable_pullCount} -Let $a \in \mathcal{A}$. The process $(N_{t,a})_{t \in \mathbb{N}}$ is predictable with respect to the filtration $\mathcal{F}$ of the algorithm-environment interaction. -\end{lemma} - -\begin{proof}\leanok - \uses{def:history,lem:pullCount_basic} - -\end{proof} - - -\begin{definition}\label{def:stepsUntil} - \uses{def:pullCount} - \leanok - \lean{Learning.stepsUntil} -For an action $a \in \mathcal{A}$ and a time $n \in \mathbb{N}$, we denote by $T_{n,a} \in \mathbb{N} \cup \{+\infty\}$ the time at which action $a$ was chosen for the $n$-th time, that is $T_{n,a} = \min\{s \in \mathbb{N} \mid N_{s+1,a} = n\}$. -Note that $T_{n, a}$ can be infinite if the action is not chosen $n$ times. -\end{definition} - -By definition, $T_{n, a}$ is the hitting time of the set $\{n\}$ by the process $t \mapsto N_{t+1,a}$, which is adapted since $N_{t,a}$ is predictable. -Equivalently, $T_{n, a}$ is the hitting time of the set $[n, +\infty]$ by that process. - - -\begin{lemma}\label{lem:stepsUntil_basic} - \uses{def:stepsUntil, def:pullCount} - \leanok - \lean{Learning.stepsUntil_zero_of_ne, Learning.stepsUntil_zero_of_eq, Learning.stepsUntil_pullCount_le, Learning.stepsUntil_pullCount_eq, Learning.action_stepsUntil, Learning.pullCount_stepsUntil_add_one, Learning.pullCount_stepsUntil} -We note the following basic properties of $T_{n,a}$: -\begin{itemize} - \item $T_{0,a} = 0$ for $a \ne A_0$. $T_{0,A_0} = \infty$. - \item $T_{N_{t+1, a}, a} \le t$. - \item $T_{N_{t + 1, A_t}, A_t} = t$. - \item If $T_{n, a} \ne \infty$ and $n > 0$, then $A_{T_{n, a}} = a$. - \item If $T_{n, a} \ne \infty$, then $N_{T_{n, a} + 1, a} = n$. - \item If $T_{n, a} \ne \infty$ and $n > 0$, then $N_{T_{n, a}, a} = n - 1$. - \item If for all $s \le t$, $A_s(\omega) = A_s(\omega')$, then $T_{n, a}(\omega) = t \iff T_{n, a}(\omega') = t$. -\end{itemize} -\end{lemma} - -\begin{proof}\leanok - \uses{lem:pullCount_basic,def:pullCount} - -\end{proof} - - -\begin{lemma}\label{lem:isStoppingTime_stepsUntil} - \uses{def:IsAlgEnvSeq.filtration, def:stepsUntil} - \leanok - \lean{Learning.isStoppingTime_stepsUntil} -Let $a \in \mathcal{A}$. For any $n > 0$, the random variable $T_{n,a}$ is a stopping time with respect to the filtration $\mathcal{F}$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:history,lem:pullCount_basic,def:pullCount} -A hitting time of a set by an adapted process is a stopping time. -\end{proof} - - -Let $\Omega' = \mathcal{R}^{\mathbb{N} \times \mathcal{A}}$ and let $\Omega = \Omega_{\mathcal{T}} \times \Omega'$ (which will be an extension of the trajectory probability space once we choose a measure on $\Omega'$). -Let $Z_{n, a} : \Omega \to \mathcal{R}$ be the projection on the coordinate indexed by $(n,a)$ in $\Omega'$. -Extending the probability space in that way allows us to define without ambiguity the reward received when choosing an action for the $n$-th time, even if that action is never actually chosen $n$ times. - - -\begin{definition}[n\textsuperscript{th} reward]\label{def:rewardByCount} - \uses{def:stepsUntil} - \leanok - \lean{Learning.rewardByCount} -We define $Y_{n, a} = R_{T_{n,a}} \mathbb{I}\{T_{n, a} < \infty\} + Z_{n,a} \mathbb{I}\{T_{n, a} = \infty\}$, the reward received when choosing action $a$ for the $n$-th time if that time is finite, and equal to $Z_{n,a}$ otherwise. -In that expression, we see $R_{T_{n,a}}$ and $T_{n, a}$ as random variables on $\Omega$ instead of $\Omega_{\mathcal{T}}$. -\end{definition} - - -\begin{lemma}\label{lem:rewardByCount_pullCount} - \uses{def:rewardByCount, def:pullCount} - \leanok - \lean{Learning.rewardByCount_pullCount_add_one_eq_reward} -$Y_{N_{t, A_t} + 1, A_t} = R_t$. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:stepsUntil_basic,def:stepsUntil} -This is perhaps hard to parse at first sight, but it follows directly from the definitions. -At time $t$, the action chosen is $A_t$ and we see a reward $R_t$. -That action had already been chosen $N_{t, A_t}$ times before time $t$, so the reward $R_t$ is the reward received when choosing action $A_t$ for the $(N_{t, A_t} + 1)$-th time, which is $Y_{N_{t, A_t} + 1, A_t}$ by definition. -\end{proof} - - -% \begin{lemma}\label{lem:measurable_rewardByCount_mul_indicator} -% \uses{def:rewardByCount, def:stepsUntil} -% $Y_{n, a} \mathbb{I}\{T_{n, a} < \infty\}$ is $\mathcal{F}_{T_{n, a}}$-measurable. -% \end{lemma} - -% \begin{proof} -% It is the stopped value of the adapted process $(R_t)_{t \in \mathbb{N}}$ at the stopping time $T_{n, a}$. -% \end{proof} - - -\section{Scalar rewards} - -TODO: change the name ``reward'' to ``observation'' throughout the chapter? - -We now focus on the case where the reward space is $\mathcal{R} = \mathbb{R}$. - - -\begin{definition}[Sum of rewards]\label{def:sumRewards} - \leanok - \lean{Learning.sumRewards} -Let $S_{t, a} = \sum_{s=0}^{t-1} R_s \mathbb{I}\{A_s = a\}$ be the sum of the rewards obtained by chosing action $a$ before time $t$. -\end{definition} - - -\begin{definition}[Empirical mean]\label{def:empMean} - \uses{def:sumRewards, def:pullCount} - \leanok - \lean{Learning.empMean} -Let $\hat{\mu}_{t, a} = \frac{S_{t, a}}{N_{t, a}} = \frac{1}{N_{t,a}} \sum_{s=0}^{t-1} R_s \mathbb{I}\{A_s = a\}$ if $N_{t, a} > 0$, and $\hat{\mu}_{t, a} = 0$ otherwise. -This is the empirical mean of the rewards obtained by choosing action $a$ before time $t$. -\end{definition} - -Note: in bandit papers it is common to (implicitly) define the empirical mean as $+\infty$ when the action was never chosen, but in Lean it has to be a real number, and the Lean default value for division by zero is $0$. - - -\begin{lemma}\label{lem:isPredictable_sumRewards} - \uses{def:IsAlgEnvSeq.filtration, def:sumRewards, def:empMean} - \leanok - \lean{Learning.IsAlgEnvSeq.isPredictable_sumRewards, Learning.IsAlgEnvSeq.isPredictable_empMean} -The processes $(S_{t,a})_{t \in \mathbb{N}}$ and $(\hat{\mu}_{t,a})_{t \in \mathbb{N}}$ are predictable with respect to the filtration $\mathcal{F}$ of the algorithm-environment interaction. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:predictable_pullCount,def:sumRewards,def:empMean} - -\end{proof} - - -The following lemma is very useful to relate the two ways of indexing the rewards: by time step and by pull count. - -\begin{lemma}\label{lem:sum_rewardByCount} - \uses{def:rewardByCount, def:pullCount, def:sumRewards} - \leanok - \lean{Learning.sum_rewardByCount_eq_sumRewards} -The sum of the first $N_{t, a}$ rewards received when choosing action $a$ is equal to the sum of the rewards obtained by choosing action $a$ before time $t$: -\begin{align*} - \sum_{n=1}^{N_{t, a}} Y_{n, a} = S_{t,a} - \: . -\end{align*} -\end{lemma} - -\begin{proof}\leanok - \uses{lem:rewardByCount_pullCount} - -\end{proof} diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex deleted file mode 100644 index 8577f8b8..00000000 --- a/blueprint/src/chapters/bandit.tex +++ /dev/null @@ -1,723 +0,0 @@ -\chapter{Stochastic multi-armed bandits} - -\section{Algorithm, bandit and probability space} - -A bandit algorithm is an algorithm in the sense of Definition~\ref{def:algorithm}. -We call the actions \emph{arms} and the observations \emph{rewards}. - -The first arm pulled by the algorithm is sampled from $P_0$, the arm pulled at time $1$ is sampled from $\pi_0(H_0)$, where $H_0 \in \mathcal{A} \times \mathcal{R}$ is the data of the first arm pulled and the first observation received, and so on. - - -\begin{definition}[Bandit]\label{def:bandit} - \uses{def:stationaryEnv} - \leanok -A stochastic bandit is simply a reward distribution for each arm: a Markov kernel $\nu : \mathcal{A} \rightsquigarrow \mathbb{R}$, conditional distribution of the rewards given the arm pulled. -It is a stationary environment in which the observation space is $\mathcal{R} = \mathbb{R}$. -\end{definition} - -An algorithm can interact with a bandit to produce a sequence of arms and rewards: after a time $t$, the history $H_t \in (\mathcal{A} \times \mathcal{R})^{t+1}$ contains the arms pulled and rewards received up to that time, -\begin{itemize} - \item the algorithm chooses an arm $A_{t+1}$ sampled according to its policy $\pi_t(H_t)$, - \item the bandit generates a reward $R_{t+1}$ according to the distribution $\nu(A_{t+1})$, - \item the history is updated to $H_{t+1} = ((A_0, R_0), \ldots, (A_{t+1}, R_{t+1}))$. -\end{itemize} - - -\section{The array model of rewards} - -We previously built a probability space on which we can define the sequence of arms and rewards generated by the interaction between the algorithm and the bandit, using the Ionescu-Tulcea theorem. -From Theorem~\ref{thm:isAlgEnvSeq_unique}, we know that the law of the sequence of arms and rewards is independent of the probability space used to define them. -Nonetheless, we now build an alternative model of the rewards, on which it will be easier to prove concentration inequalities. -By the uniqueness of the law, these statements will then transfer to any algorithm-environment interaction. - -In the ``array model'', we consider a probability space on which we have an infinite array of rewards from each arm, independent from each other. -When pulling an arm, the algorithm sees the next previously unseen reward from that arm in the array. - -\begin{definition}\label{def:arrayMeasure} - \uses{thm:ionescu-tulcea} % because it uses infinitePi - \leanok - \lean{Bandits.ArrayModel.probSpace, Bandits.ArrayModel.arrayMeasure} -Let $I = [0,1]$ and let $P_U$ be the uniform distribution on $I$. We define the probability space $(\Omega_{\mathcal{A}}, P_{\mathcal{A}})$, where -\begin{align*} - \Omega_{\mathcal{A}} &:= I^{\mathbb{N}} \times \mathcal{R}^{\mathbb{N} \times \mathcal{A}} - \: , \\ - P_{\mathcal{A}} &:= \left( \bigotimes_{n \in \mathbb{N}} P_U \right) \otimes \left( \bigotimes_{n \in \mathbb{N}, a \in \mathcal{A}} \nu(a) \right) - \: . -\end{align*} -\end{definition} - - -\begin{definition}\label{def:algFunction} - \uses{def:algorithm} - \leanok - \lean{Bandits.ArrayModel.algFunction, Bandits.ArrayModel.initAlgFunction} -Let $\mathfrak{A}$ be an algorithm with action space $\mathcal{A}$ and reward space $\mathcal{R}$, policy $\pi$ and initial distribution $P_0$. -For $\mathcal{A}$ and $\mathcal{R}$ standard Borel spaces, there exists jointly measurable functions $f'_0 : I \to \mathcal{A}$ and $f_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times I \to \mathcal{A}$ such that -\begin{itemize} - \item the law of $f'_0$ is $P_0$, - \item for all history $h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}$, the law of $f_t(h_t, \cdot)$ is $\pi_t(h_t)$. -\end{itemize} -\end{definition} - - -\begin{definition}\label{def:AM.history} - \uses{def:algFunction, def:arrayMeasure, def:pullCount} - \leanok - \lean{Bandits.ArrayModel.hist, Bandits.ArrayModel.action, Bandits.ArrayModel.reward} -The history, actions and rewards on the array model probability space $(\Omega_{\mathcal{A}}, P_{\mathcal{A}})$ are defined as follows: -\begin{itemize} - \item the action at time $0$ is $A_0(\omega) = f'_0(\omega_{1,0})$, the reward at time $0$ is $R_0(\omega) = \omega_{2,0,A_0(\omega)}$, and the history at time $0$ is $H_0(\omega) = (A_0(\omega), R_0(\omega))$, - \item for $t \ge 0$, the action at time $t+1$ is $A_{t+1}(\omega) = f_t(H_t(\omega), \omega_{1,t+1})$, the reward at time $t+1$ is $R_{t+1}(\omega) = \omega_{2,N_{t+1,A_{t+1}(\omega)},A_{t+1}(\omega)}$, and the history at time $t+1$ is $H_{t+1}(\omega) = (H_t(\omega), (A_{t+1}(\omega), R_{t+1}(\omega)))$. -\end{itemize} -\end{definition} - - -The goal of this section is to show that $(\Omega_{\mathcal{A}}, P_{\mathcal{A}})$ with the actions and rewards defined above is an algorithm-environment sequence as in Definition~\ref{def:IsAlgEnvSeq}. - - -\subsection{Measurability} - -TODO: some of those results are proved for $\mathcal{A}$ countable. Add that assumption where needed. - -\begin{remark}[Proving measurability with respect to a sub-sigma-algebra] -In this section, we often need to prove that a random variable $X$ is measurable with respect to the sigma-algebra generated by a subset of the independent random variables defining the probability space $\Omega_{\mathcal{A}}$. -We want to prove that $X : \Omega_{\mathcal{A}} \to \mathcal{X}$ is measurable with respect to the sigma-algebra $\sigma((\omega_p)_{p \in S})$, where $S$ is a subset of the indices of the independent random variables defining $\Omega_{\mathcal{A}}$. -In most cases, this is due to $X$ being defined (possibly recursively in a complicated way) only using those random variables. -However, it might be difficult to exhibit an explicit function $f$ such that $X = f((\omega_p)_{p \in S})$. - -Here is a general strategy to prove such measurability results in Lean: -\begin{enumerate} - \item Prove that $X$ is measurable with respect to the full sigma-algebra on $\Omega_{\mathcal{A}}$. - \item Prove a congruence lemma: for any $\omega, \omega' \in \Omega_{\mathcal{A}}$, if $\omega_p = \omega'_p$ for all $p \in S$, then $X(\omega) = X(\omega')$. - \item Define $g : (\prod_{p \in S} \Omega_p) \to \Omega$ by $g((\omega_p)_{p \in S}) = \omega'$, where $\omega'_p = \omega_p$ for $p \in S$ and $\omega'_p$ is some fixed value for $p \notin S$. - \item Write $X = X \circ g \circ \mathrm{proj}_S$, where $\mathrm{proj}_S : \Omega_{\mathcal{A}} \to \prod_{p \in S} \Omega_p$ is the projection on the coordinates in $S$. - \item Conclude that $X$ is the composition of a measurable function $(X \circ g)$ and the random variable generating the sub-sigma-algebra, and thus is measurable with respect to that sub-sigma-algebra. -\end{enumerate} -\end{remark} - -\begin{lemma}[Measurability]\label{lem:AM.measurable_hist} - \uses{def:AM.history,def:arrayMeasure,def:algorithm} -\leanok - \lean{Bandits.ArrayModel.measurable_hist, Bandits.ArrayModel.measurable_action, Bandits.ArrayModel.measurable_reward} -$H_t$, $N_{t,A_t}$, $A_t$ and $R_t$ are measurable for all $t \in \mathbb{N}$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:algFunction,def:AM.history} - -\end{proof} - - -\begin{lemma}[Congruence for the history]\label{lem:AM.hist_congr} - \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:pullCount} - \leanok - \lean{Bandits.ArrayModel.hist_congr} -Let $\omega, \omega' \in \Omega_{\mathcal{A}}$ and $t \in \mathbb{N}$. -Suppose that -\begin{align*} - \forall s \le t, \ \omega_{1,s} &= \omega'_{1,s} - \: , \\ - \forall a \in \mathcal{A}, \forall s < N_{t+1,a}, \ \omega_{2,s,a} &= \omega'_{2,s,a} - \: . -\end{align*} -Then $H_t(\omega) = H_t(\omega')$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:AM.history,def:algFunction,lem:pullCount_basic} - -\end{proof} - - -\begin{lemma}[Congruence for the number of pulls and action]\label{lem:AM.stepsUntil_congr} - \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:pullCount} -\leanok - \lean{Bandits.ArrayModel.stepsUntil_congr} -Let $\omega, \omega' \in \Omega_{\mathcal{A}}$, $t, m \in \mathbb{N}$ and $a \in \mathcal{A}$. -Suppose that -\begin{align*} - \omega_{1} &= \omega'_{1} - \: , \\ - \forall s < m, \ \omega_{2,s,a} &= \omega'_{2,s,a} - \: , \\ - \forall b \ne a, \forall s \in \mathbb{N}, \ \omega_{2,s,b} &= \omega'_{2,s,b} - \: . -\end{align*} -Then $(N_{t+1, a}(\omega) = m \wedge A_{t+1}(\omega) = a) \iff (N_{t+1, a}(\omega') = m \wedge A_{t+1}(\omega') = a)$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:AM.history,def:algFunction,lem:AM.hist_congr} - -\end{proof} - - -\begin{definition}\label{def:AM.probSpaceSubsets} - \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:pullCount} - \leanok - \lean{Bandits.ArrayModel.truePast} -We define the following functions on $\Omega_{\mathcal{A}}$: -\begin{align*} - F_{1, t}(\omega) &= ((\omega_{1,s})_{s \le t}, (\omega_{2,s})_{s \in \mathbb{N}}) - \: , \\ - F_{2, a, t}(\omega) &= ((\omega_{1,s})_{s \in \mathbb{N}}, (\omega_{2, \min\{s,N_{t+1,a}(\omega)-1\}, a})_{s \in \mathbb{N}}, (\omega_{2, s, b})_{s \in \mathbb{N}, b \ne a}) - \: , \\ - F_{2, a}^m(\omega) &= ((\omega_{1,s})_{s \in \mathbb{N}}, (\omega_{2, \min\{s,m-1\}, a})_{s \in \mathbb{N}}, (\omega_{2, s, b})_{s \in \mathbb{N}, b \ne a}) - \: . -\end{align*} -In the definition of $F_{2, a, t}$ and $F_{2, a}^m$, if $N_{t+1,a}(\omega) = 0$ (resp. $m = 0$), then the second component is a constant sequence equal to an arbitrary value. - -$F_{1, t}(\omega)$ contains all the information in $\omega$ except for the action selection randomness after time $t$. - -$F_{2, a, t}(\omega)$ contains all the information in $\omega$ except the rewards for arm $a$ indexed by $N_{t+1,a}(\omega)$ or more. -$F_{2, a}^m(\omega)$ is similar, but removes the rewards for arm $a$ indexed by $m$ or more. -\end{definition} - - -\begin{lemma}\label{lem:AM.measurable_hist_comap} - \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:AM.probSpaceSubsets} -\leanok - \lean{Bandits.ArrayModel.measurable_hist_comap, Bandits.ArrayModel.measurable_hist_truePast} -For all $t \in \mathbb{N}$, $H_t$ is measurable with respect to the sigma-algebra generated by $F_{1, t}$, and with respect to the sigma-algebra generated by $F_{2, a, t}$ for any arm $a \in \mathcal{A}$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:AM.history,lem:AM.measurable_hist,def:pullCount,lem:AM.hist_congr} - -\end{proof} - - -\begin{lemma}\label{lem:AM.measurable_action_add_one_truePast} - \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:AM.probSpaceSubsets} - \leanok - \lean{Bandits.ArrayModel.measurable_action_add_one_truePast} -$A_{t+1}$ is measurable with respect to the sigma-algebra generated by $F_{2, a, t}$ for any arm $a \in \mathcal{A}$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:AM.history,lem:AM.measurable_hist_comap,def:algFunction} - -\end{proof} - - -\begin{lemma}\label{lem:AM.measurable_pullCount_add_one_truePast} - \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:AM.probSpaceSubsets,def:pullCount} - \leanok - \lean{Bandits.ArrayModel.measurable_pullCount_add_one_truePast} -$N_{t+1,a}$ is measurable with respect to the sigma-algebra generated by $F_{2, a, t}$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:AM.history,lem:AM.measurable_hist_comap,def:algFunction} - -\end{proof} - - -\begin{lemma}\label{lem:AM.measurable_stepsUntil} - \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:pullCount,def:AM.probSpaceSubsets} -\leanok - \lean{Bandits.ArrayModel.measurable_stepsUntil} -For $t, m \in \mathbb{N}$ and $a \in \mathcal{A}$, the indicator function $\mathbb{I}\{N_{t+1,a} = m \wedge A_{t+1} = a\} : \Omega_{\mathcal{A}} \to \{0, 1\}$ is measurable with respect to the sigma-algebra generated by $F_{2, a}^m$. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:AM.measurable_hist,lem:AM.stepsUntil_congr} - -\end{proof} - - -\begin{lemma}\label{lem:AM.measurable_pullCount_action_add_one_hist} - \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:pullCount} -\leanok - \lean{Bandits.ArrayModel.measurable_pullCount_action_add_one_hist} -For $t \in \mathbb{N}$, the function $N_{t+1, A_{t+1}}$ is measurable with respect to the sigma-algebra generated by $H_t$ and $A_{t+1}$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:algFunction} - -\end{proof} - - -\subsection{Independence} - - -\begin{lemma}\label{lem:AM.indepFun_fst_add_one_aux} - \uses{def:AM.probSpaceSubsets, def:arrayMeasure} - \leanok - \lean{Bandits.ArrayModel.indepFun_fst_add_one_aux} -$\omega \mapsto \omega_{1, t+1}$ is independent of $F_{1, t}$. -\end{lemma} - -\begin{proof}\leanok - \uses{thm:ionescu-tulcea} - -\end{proof} - - -\begin{lemma}\label{lem:AM.indepFun_fst_add_one_hist} - \uses{def:AM.history,def:AM.probSpaceSubsets, def:arrayMeasure,def:algorithm} - \leanok - \lean{Bandits.ArrayModel.indepFun_fst_add_one_hist} -$\omega \mapsto \omega_{1, t+1}$ is independent of $H_t$. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:AM.measurable_hist_comap,lem:AM.indepFun_fst_add_one_aux} - -\end{proof} - - -\begin{lemma}\label{lem:AM.indepFun_snd_apply_aux} - \uses{def:arrayMeasure,def:AM.probSpaceSubsets} - \leanok - \lean{Bandits.ArrayModel.indepFun_snd_apply_aux} -For $a \in \mathcal{A}$ and $m \in \mathbb{N}$, $\omega \mapsto \omega_{2, m, a}$ is independent of $F_{2, a}^m$. -\end{lemma} - -\begin{proof}\leanok - \uses{thm:ionescu-tulcea} - -\end{proof} - - -\begin{lemma}\label{lem:AM.indepFun_snd_apply_pullCount_action} - \uses{def:arrayMeasure,def:AM.history,def:algorithm,def:pullCount,def:AM.probSpaceSubsets} - \leanok - \lean{Bandits.ArrayModel.indepFun_snd_apply_pullCount_action} -For $a \in \mathcal{A}$, $\omega \mapsto \omega_{2, m, a}$ is independent of the indicator function $\mathbb{I}\{N_{t+1,a} = m \wedge A_{t+1} = a\}$. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:AM.indepFun_snd_apply_aux,lem:AM.measurable_stepsUntil} - -\end{proof} - - -\begin{lemma}\label{lem:AM.indepFun_snd_hist_cond} - \uses{def:arrayMeasure,def:AM.history,def:algorithm,def:pullCount} - \leanok - \lean{Bandits.ArrayModel.indepFun_snd_hist_cond} -For $a \in \mathcal{A}$ and $t, m \in \mathbb{N}$, $\omega \mapsto \omega_{2, m, a}$ is independent of $H_t$ given that $N_{t+1,a} = m$ and $A_{t+1} = a$. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:AM.measurable_hist_comap,lem:AM.measurable_hist,lem:AM.indepFun_snd_apply_aux,lem:AM.measurable_stepsUntil,def:AM.probSpaceSubsets} - -\end{proof} - - -\subsection{Laws} - - -\begin{lemma}\label{lem:AM.hasLaw_action_zero} - \uses{def:arrayMeasure,def:AM.history,def:algorithm} -\leanok - \lean{Bandits.ArrayModel.hasLaw_action_zero} -The law of $A_0$ in the array model is $P_0$. -\end{lemma} - -\begin{proof}\leanok - \uses{thm:ionescu-tulcea,def:algFunction,lem:AM.measurable_hist} - -\end{proof} - - -\begin{lemma}\label{lem:AM.hasCondDistrib_reward_zero} - \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea} - \leanok - \lean{Bandits.ArrayModel.hasCondDistrib_reward_zero} -In the array model, $P_{\mathcal{A}}(R_0 \mid A_0) = \nu$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:algFunction,lem:AM.measurable_hist,lem:condDistrib_ae_eq_cond} - -\end{proof} - - -\begin{lemma}\label{lem:AM.hasCondDistrib_action} - \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea} - \leanok - \lean{Bandits.ArrayModel.hasCondDistrib_action} -In the array model, $P_{\mathcal{A}}(A_{t+1} \mid H_t) = \pi_t$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:AM.history,def:algFunction,lem:AM.measurable_hist,lem:AM.indepFun_fst_add_one_hist} - -\end{proof} - - -\begin{lemma}\label{lem:AM.hasCondDistrib_reward_pullCount_action} - \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea,def:pullCount} -\leanok - \lean{Bandits.ArrayModel.hasCondDistrib_reward_pullCount_action} -In the array model, $P_{\mathcal{A}}(R_{t+1} \mid N_{t+1,A_{t+1}}, A_{t+1}) = \nu$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:AM.history,lem:AM.indepFun_snd_apply_pullCount_action,def:algFunction,lem:AM.measurable_hist,lem:pullCount_basic,lem:condDistrib_ae_eq_cond} - -\end{proof} - - -\begin{lemma}\label{lem:AM.hasCondDistrib_reward_hist_action_pullCount} - \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea,def:pullCount} -\leanok - \lean{Bandits.ArrayModel.hasCondDistrib_reward_hist_action_pullCount} -In the array model, $P_{\mathcal{A}}(R_{t+1} \mid H_t, A_{t+1}, N_{t+1,A_{t+1}}) = \nu$. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:AM.indepFun_snd_apply_pullCount_action,lem:AM.indepFun_snd_hist_cond,def:algFunction,lem:AM.measurable_hist,lem:pullCount_basic} - -\end{proof} - - -\begin{lemma}\label{lem:AM.condIndepFun_reward_hist} - \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea,lem:AM.measurable_hist,def:pullCount} - \leanok - \lean{Bandits.ArrayModel.condIndepFun_reward_hist} -For $t \ge 0$, $R_{t+1} \ind H_t \mid A_{t+1}, N_{t+1, A_{t+1}}$. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:AM.measurable_hist,lem:AM.hasCondDistrib_reward_hist_action_pullCount} - -\end{proof} - - -\begin{lemma}\label{lem:AM.hasCondDistrib_reward} - \uses{def:arrayMeasure,def:AM.history,def:stationaryEnv,def:environment,def:algorithm,thm:ionescu-tulcea} - \leanok - \lean{Bandits.ArrayModel.hasCondDistrib_reward} -In the array model, $P_{\mathcal{A}}(R_{t+1} \mid H_t, A_{t+1}) = \nu$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:AM.history,lem:AM.measurable_pullCount_action_add_one_hist,lem:AM.hasCondDistrib_reward_pullCount_action,def:algFunction,lem:AM.measurable_hist,lem:AM.condIndepFun_reward_hist,def:pullCount} - -\end{proof} - -\begin{theorem}\label{thm:isAlgEnvSeq_arrayMeasure} - \uses{def:arrayMeasure,def:AM.history,def:stationaryEnv,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea} - \leanok - \lean{Bandits.ArrayModel.isAlgEnvSeq_arrayMeasure} -The actions and rewards defined on the array model probability space $(\Omega_{\mathcal{A}}, P_{\mathcal{A}})$ form an algorithm-environment sequence for the algorithm $\mathfrak{A}$ and bandit $\nu$. -\end{theorem} - -\begin{proof}\leanok - \uses{lem:AM.hasCondDistrib_action,def:environment,lem:AM.hasCondDistrib_reward,lem:AM.measurable_hist,def:history,lem:AM.hasLaw_action_zero,lem:AM.hasCondDistrib_reward_zero} -The four conditions of Definition~\ref{def:IsAlgEnvSeq} are satisfied by Lemmas~\ref{lem:AM.hasLaw_action_zero}, \ref{lem:AM.hasCondDistrib_reward_zero}, \ref{lem:AM.hasCondDistrib_action} and \ref{lem:AM.hasCondDistrib_reward}. -\end{proof} - - - - -\section{Law of the n\textsuperscript{th} pull}\label{sec:alt_model} - -This section describes the law of $Y_{n, a}$ the $n^{th}$ reward obtained from an arm $a \in \mathcal{A}$ (Definition~\ref{def:rewardByCount}). - -We augment the probability space $\Omega$ on which we have an algorithm-environment sequence with $\Omega' = \mathbb{R}^{\mathbb{N} \times \mathcal{A}}$, on which we put the product measure $\bigotimes_{n \in \mathbb{N}, a \in \mathcal{A}} \nu(a)$. -With that measure, the law of $Z_{n,a}$ is $\nu(a)$. - - -\begin{lemma}\label{lem:measurable_comap_indicator_stepsUntil_eq} - \uses{def:history,def:stepsUntil} - \leanok - \lean{Learning.measurable_comap_indicator_stepsUntil_eq} -The function $\mathbb{I}\{T_{n,a} = t\} : \Omega \to \{0, 1\}$ is measurable with respect to the sigma-algebra generated by $(H_{t-1}, A_t)$. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:stepsUntil_basic,lem:pullCount_basic,def:pullCount,def:IsAlgEnvSeq.filtration} - -\end{proof} - - -\begin{lemma}\label{lem:condIndepFun_reward_stepsUntil_arm} - \uses{def:stationaryEnv,def:environment,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea,def:stepsUntil} - \leanok - \lean{Bandits.condIndepFun_reward_stepsUntil_action} -For $t > 0$, $R_t \ind \mathbb{I}\{T_{n, a} = t\} \mid A_t$. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:condIndepFun_reward_hist_action,lem:CondIndepFun.prod_right,lem:stepsUntil_basic,lem:measurable_comap_indicator_stepsUntil_eq,def:history,def:pullCount} -$\mathbb{I}\{T_{n, a} = t\}$ is measurable with respect to the sigma-algebra generated by $(H_{t-1}, A_t)$ by Lemma~\ref{lem:measurable_comap_indicator_stepsUntil_eq}. - -It thus suffices to show that $R_t \ind (H_{t-1}, A_t) \mid A_t$, which is implied by $R_t \ind H_{t-1} \mid A_t$ (Lemma~\ref{lem:CondIndepFun.prod_right}), which is Lemma~\ref{lem:condIndepFun_reward_hist_action}. -\end{proof} - - -\begin{lemma}\label{lem:reward_cond_stepsUntil} - \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea,def:stepsUntil} - \leanok - \lean{Bandits.reward_cond_stepsUntil} -Let $n > 0$, $t \in \mathbb{N}$ and suppose that $P(T_{n, a} = t) > 0$. -Then $P(R_t \mid T_{n, a} = t) = \nu(a)$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:environment,lem:stepsUntil_basic,lem:condIndepFun_reward_stepsUntil_arm,def:pullCount,lem:condDistrib_ae_eq_cond,lem:condDistrib_reward_stationaryEnv} -First, if $T_{n, a} = t$, then $A_t = a$ (Lemma~\ref{lem:stepsUntil_basic}), such that $P(R_t \mid T_{n, a} = t) = P(R_t \mid T_{n, a} = t, A_t = a)$. - -Then, using first the independence from Lemma~\ref{lem:condIndepFun_reward_stepsUntil_arm} and then the conditional distribution from Lemma~\ref{lem:condDistrib_reward_stationaryEnv}, we have -\begin{align*} - P(R_t \mid T_{n, a} = t, A_t = a) - &= P(R_t \mid A_t = a) - = \nu(a) - \: . -\end{align*} -\end{proof} - - -\begin{lemma}\label{lem:condDistrib_ae_eq_cond} - \leanok - \lean{ProbabilityTheory.condDistrib_ae_eq_cond} -For a random variable $X$ on a countable space with the discrete sigma algebra, $P(Y \mid X) = (x \mapsto P(Y \mid X = x))$, $(X_*P)$-almost surely. -Furthermore, that almost sure equality means that for all $x$ such that $P(X = x) > 0$, we have $P(Y \mid X = x) = P(Y \mid X)(x)$. -\end{lemma} - -\begin{proof}\leanok - -\end{proof} - - -\begin{lemma}\label{lem:condDistrib_rewardByCount_stepsUntil} - \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea,def:rewardByCount,def:stepsUntil} -\leanok - \lean{Bandits.condDistrib_rewardByCount_stepsUntil} -For $n > 0$ and $t \in \mathbb{N}$, $P(Y_{n,a} \mid T_{n,a}) = \nu(a)$ (in which the measure on the r.h.s. is seen as a constant kernel). -\end{lemma} - -\begin{proof}\leanok - \uses{def:environment,lem:reward_cond_stepsUntil,def:pullCount,lem:condDistrib_ae_eq_cond} -It suffices to show that for all $t \in \mathbb{N} \cup \{\infty\}$ such that $P(T_{n, a} = t) > 0$, the law of $Y_{n,a}$ conditioned on $T_{n,a} = t$ is $\nu(a)$. - -If $t < \infty$, then $P(Y_{n, a} \mid T_{n, a} = t) = P(R_t \mid T_{n, a} = t) = \nu(a)$ by Lemma~\ref{lem:reward_cond_stepsUntil}. - -If $t = \infty$, then $P(Y_{n, a} \mid T_{n, a} = \infty) = P(Z_{n, a} \mid T_{n, a} = \infty)$. By independence of $Z_{n,a}$ and $T_{n, a}$, this is just $\nu(a)$, the law of $Z_{n,a}$. -\end{proof} - - -\begin{lemma}\label{lem:hasLaw_rewardByCount} - \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea,def:rewardByCount} - \leanok - \lean{Bandits.hasLaw_rewardByCount} -For $n > 0$ and $a \in \mathcal{A}$, $(Y_{n,a})_*P = \nu(a)$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:environment,lem:condDistrib_rewardByCount_stepsUntil,def:stepsUntil,def:pullCount} -The law of $Y_{n,a}$ is given by $(Y_{n, a})_*P = P(Y_{n, a} \mid T_{n, a}) \circ (T_{n, a})_*P$. -By Lemma~\ref{lem:condDistrib_rewardByCount_stepsUntil}, $P(Y_{n, a} \mid T_{n, a}) = \nu(a)$, a constant kernel. -Thus the composition is just $\nu(a)$. -\end{proof} - - -% \begin{lemma}\label{lem:indepFun_rewardByCount_stepsUntil} -% \uses{def:stepsUntil, def:rewardByCount, def:Bandit.measure} -% For $n > 0$, $Y_{n, a} \ind T_{n,a}$. -% \end{lemma} - -% \begin{proof} -% \uses{lem:condDistrib_rewardByCount_stepsUntil, lem:hasLaw_rewardByCount} -% It suffices to prove that $\mathcal{L}(Y_{n,a} \mid T_{n,a}) = \mathcal{L}(Y_{n,a})$. - -% By Lemma~\ref{lem:hasLaw_rewardByCount}, $\mathcal{L}(Y_{n,a}) = \nu(a)$. -% By Lemma~\ref{lem:condDistrib_rewardByCount_stepsUntil}, $\mathcal{L}(Y_{n,a} \mid T_{n,a}) = \nu(a)$. -% \end{proof} - - -% \begin{lemma}\label{lem:condIndepFun_rewardByCount_hist} -% \uses{def:rewardByCount, def:stepsUntil, def:Bandit.measure} -% For $n > 0$, $Y_{n, a} \ind H_{T_{n,a}-1} \mid T_{n,a}$, in which $H_{\infty}$ is interpreted as the whole history. -% \end{lemma} - -% \begin{proof} -% \uses{lem:condDistrib_rewardByCount_stepsUntil, lem:condIndepFun_reward_hist_action} -% By Lemma~\ref{lem:condDistrib_rewardByCount_stepsUntil}, $\mathcal{L}(Y_{n,a} \mid T_{n,a}) = \nu(a)$. -% We need to prove that $\mathcal{L}(Y_{n,a} \mid H_{T_{n,a}-1}, T_{n,a}) = \nu(a)$. -% By Lemma~\ref{lem:stepsUntil_basic}, if $T_{n,a} = t \in \mathbb{N}$, then $A_t = a$. -% We get -% \begin{align*} -% \mathcal{L}(Y_{n,a} \mid H_{T_{n,a}-1}, T_{n,a} = t) -% &= \mathcal{L}(R_t \mid H_{t-1}, T_{n,a} = t, A_t = a) -% \: . -% \end{align*} -% Then, $\mathbb{I}\{T_{n,a} = t\}$ is a function of $(H_{t-1}, A_t)$ by Lemma~\ref{lem:measurable_comap_indicator_stepsUntil_eq}, such that - -% \begin{align*} -% \mathcal{L}(R_t \mid H_{t-1}, T_{n,a} = t, A_t = a) -% &= \mathcal{L}(R_t \mid H_{t-1}, A_t = a) -% \: . -% \end{align*} -% Thus, using Lemma~\ref{lem:condIndepFun_reward_hist_action}, we have -% \begin{align*} -% \mathcal{L}(R_t \mid H_{t-1}, A_t = a) -% = \nu(a) -% \: . -% \end{align*} - -% If $T_{n,a} = \infty$, then $\mathcal{L}(Y_{n,a} \mid H_{T_{n,a}-1}, T_{n,a} = \infty) = \mathcal{L}(Z_{n,a} \mid H_{\infty}, T_{n,a} = \infty) = \nu(a)$ by independence of $Z_{n,a}$ from the history and $T_{n,a}$. - -% \end{proof} - - -% \begin{lemma}\label{lem:indepFun_rewardByCount_hist_stepsUntil} -% \uses{def:rewardByCount, def:stepsUntil, def:Bandit.measure} -% For $n > 0$, $Y_{n, a} \ind (H_{T_{n,a}-1}, T_{n,a})$. -% \end{lemma} - -% \begin{proof} -% \uses{lem:condIndepFun_rewardByCount_hist} -% By Lemma~\ref{lem:condIndepFun_rewardByCount_hist}, $Y_{n, a} \ind H_{T_{n,a}-1} \mid T_{n,a}$. -% By Lemma~\ref{lem:indepFun_rewardByCount_stepsUntil}, $Y_{n, a} \ind T_{n,a}$. -% By the contraction property of conditional independence (Lemma~\ref{lem:indepFun_contraction}), we have $Y_{n, a} \ind (H_{T_{n,a}-1}, T_{n,a})$. -% \end{proof} - - -% \begin{lemma}\label{lem:iIndepFun_rewardByCount} -% \uses{def:rewardByCount} -% The rewards $(Y_{n,a})_{n \in \mathbb{N}}$ are independent. -% \end{lemma} - -% \begin{proof} -% \uses{lem:iIndepFun_nat_iff_forall_indepFun, lem:indepFun_contraction, lem:indepFun_rewardByCount_stepsUntil} -% By Lemma~\ref{lem:iIndepFun_nat_iff_forall_indepFun}, it suffices to show that for all $n \in \mathbb{N}$, $Y_{n+1, a}$ is independent of $(Y_{1,a}, \ldots, Y_{n,a})$. - -% By the contraction property of conditional independence (Lemma~\ref{lem:indepFun_contraction}), it suffices to show that $Y_{n+1, a}$ is independent of $(Y_{1,a}, \ldots, Y_{n,a})$ conditionally on $T_{n+1, a}$ and that $Y_{n+1, a}$ is independent of $T_{n+1, a}$. - -% The fact that $Y_{n+1, a}$ is independent of $T_{n+1, a}$ is Lemma~\ref{lem:indepFun_rewardByCount_stepsUntil}. - -% TODO - -% \end{proof} - - -% \begin{lemma}\label{lem:independent_rewardByCount} -% \uses{def:rewardByCount} -% For $a \in \mathcal{A}$, let $Y^{(a)} = (Y_{n,a})_{n \in \mathbb{N}} \in \mathbb{R}^{\mathbb{N}}$ be the sequence of rewards obtained from pulling arm $a$. Then the sequences $(Y^{(a)})_{a \in \mathcal{A}}$ are independent. -% \end{lemma} - -% \begin{proof} - -% \end{proof} - - -% \begin{lemma}\label{lem:identDistrib_rewardByCount_stream} -% \uses{def:rewardByCount} -% The random sequences $(Y_{n+1,a})_{n \in \mathbb{N}}$ and $(Z_{n,a})_{n \in \mathbb{N}}$ are identically distributed. -% \end{lemma} - -% \begin{proof} -% \uses{lem:hasLaw_rewardByCount, lem:iIndepFun_rewardByCount} - -% \end{proof} - - -% \begin{lemma}\label{lem:identDistrib_sum_Icc_rewardByCount} -% \uses{def:rewardByCount} -% The random variables $\sum_{i=1}^n Y_{i,a}$ and $\sum_{i=0}^{n-1} Z_{i,a}$ are identically distributed. -% \end{lemma} - -% \begin{proof} -% \uses{lem:identDistrib_rewardByCount_stream} -% Immediate consequence of Lemma~\ref{lem:identDistrib_rewardByCount_stream}. -% \end{proof} - - -\section{Regret and other bandit quantities} - -\begin{definition}[Arm means]\label{def:armMean} - \uses{def:bandit} - \leanok % no actual Lean def, but we don't need one -For an arm $a \in \mathcal{A}$, we denote by $\mu_a$ the mean of the rewards for that arm, that is $\mu_a = \nu(a)[\mathrm{id}]$. -We denote by $\mu^*$ the mean of the best arm, that is $\mu^* = \max_{a \in \mathcal{A}} \mu_a$. -\end{definition} - - -\begin{definition}[Regret]\label{def:regret} - \uses{def:armMean} - \leanok - \lean{Bandits.regret} -The regret $R_T$ of a sequence of arms $A_0, \ldots, A_{T-1}$ after $T$ pulls is the difference between the cumulative reward of always playing the best arm and the cumulative reward of the sequence: -\begin{align*} - R_T = T \mu^* - \sum_{t=0}^{T-1} \mu_{A_t} \: . -\end{align*} -\end{definition} - -TODO: the $R_T$ notation clashes with the random variable $R_t$. - -\begin{definition}\label{def:gap} - \uses{def:armMean} - \leanok - \lean{Bandits.gap} -For an arm $a \in \mathcal{A}$, its gap is defined as the difference between the mean of the best arm and the mean of that arm: $\Delta_a = \mu^* - \mu_a$. -\end{definition} - - -\begin{lemma}\label{lem:sum_pullCount_mul} - \uses{def:pullCount} - \leanok - \lean{Learning.sum_pullCount_mul} -Let $f : \mathcal{A} \to \mathbb{R}$ be a function on the arms. For all $t \in \mathbb{N}$, -\begin{align*} - \sum_{a \in \mathcal{A}} N_{t,a} f(a) = \sum_{s=0}^{t-1} f(A_s) \: . -\end{align*} -\end{lemma} - -\begin{proof}\leanok -\begin{align*} - \sum_{a \in \mathcal{A}} N_{t,a} f(a) - &= \sum_{a \in \mathcal{A}} \sum_{s=0}^{t-1} \mathbb{I}\{A_s = a\} f(a) - \\ - &= \sum_{s=0}^{t-1} \sum_{a \in \mathcal{A}} \mathbb{I}\{A_s = a\} f(a) - \\ - &= \sum_{s=0}^{t-1} f(A_s) - \: . -\end{align*} -\end{proof} - - -\begin{lemma}\label{lem:regret_eq_sum_pullCount_mul_gap} - \uses{def:regret,def:gap,def:pullCount} - \leanok - \lean{Bandits.regret_eq_sum_pullCount_mul_gap} -For $\mathcal{A}$ finite, the regret $R_T$ can be expressed as a sum over the arms and their gaps: -\begin{align*} - R_T = \sum_{a \in \mathcal{A}} N_{T,a} \Delta_a \: . -\end{align*} -\end{lemma} - -\begin{proof}\leanok - \uses{lem:sum_pullCount_mul} -Apply Lemma~\ref{lem:sum_pullCount_mul} with $f(a) = \Delta_a$ to obtain: -\begin{align*} - \sum_{a \in \mathcal{A}} N_{T,a} \Delta_a - &= \sum_{s=0}^{T-1} \Delta_{A_s} - \\ - &= \sum_{s=0}^{T-1} \mu^* - \sum_{s=0}^{T-1} \mu_{A_s} - \\ - &= R_T - \: . -\end{align*} -\end{proof} - - -\begin{corollary}\label{cor:integral_regret_eq_sum_mul} - \uses{def:regret,def:gap,def:pullCount} - \leanok - \lean{Bandits.integral_regret_eq_sum_gap_mul_integral_pullCount} -For $\mathcal{A}$ finite, the expected regret can be expressed as a sum over the arms and their gaps: -\begin{align*} - P[R_T] = \sum_{a \in \mathcal{A}}P[N_{T,a}] \Delta_a \: . -\end{align*} -\end{corollary} - -\begin{proof}\leanok - \uses{lem:regret_eq_sum_pullCount_mul_gap} - -\end{proof} diff --git a/blueprint/src/chapters/concentration.tex b/blueprint/src/chapters/concentration.tex deleted file mode 100644 index eaf2eb37..00000000 --- a/blueprint/src/chapters/concentration.tex +++ /dev/null @@ -1,197 +0,0 @@ -\chapter{Concentration inequalities} - - -\section{Sub-Gaussian random variables} - -\begin{definition}[Sub-Gaussian]\label{def:subGaussian} - \mathlibok - \lean{ProbabilityTheory.HasSubgaussianMGF} -A real valued random variable $X$ is $\sigma^2$-sub-Gaussian if for any $\lambda \in \mathbb{R}$, -\begin{align*} - P\left[e^{\lambda X}\right] - &\le e^{\frac{\lambda^2 \sigma^2}{2}} - \: . -\end{align*} -\end{definition} - - -\begin{lemma}\label{lem:subGaussian_add_of_indepFun} - \uses{def:subGaussian} - \mathlibok - \lean{ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun} -If $X$ is $\sigma_1^2$-sub-Gaussian and $Y$ is $\sigma_2^2$-sub-Gaussian, and $X$ and $Y$ are independent, then $X + Y$ is $(\sigma_1^2 + \sigma_2^2)$-sub-Gaussian. -\end{lemma} - -\begin{proof}\leanok - -\end{proof} - - -\begin{lemma}\label{lem:hoeffding_one} - \uses{def:subGaussian} - \mathlibok - \lean{ProbabilityTheory.HasSubgaussianMGF.measure_ge_le} -For $X$ a $\sigma^2$-sub-Gaussian random variable, for any $t \ge 0$, -\begin{align*} - P(X \ge t) - &\le \exp\left(- \frac{t^2}{2 \sigma^2}\right) - \: . -\end{align*} -\end{lemma} - -\begin{proof}\leanok - -\end{proof} - - -\begin{theorem}\label{thm:hoeffding} - \uses{def:subGaussian} - \mathlibok - \lean{ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun} -Let $X_1, \ldots, X_n$ be independent random variables such that $X_i$ is $\sigma_i^2$-sub-Gaussian for $i \in [n]$. -Then for any $t \ge 0$, -\begin{align*} - P\left(\sum_{i=1}^n X_i \ge t\right) - &\le \exp\left(- \frac{t^2}{2 \sum_{i=1}^n \sigma_i^2}\right) - \: . -\end{align*} -\end{theorem} - -\begin{proof}\leanok - \uses{lem:subGaussian_add_of_indepFun, lem:hoeffding_one} - -\end{proof} - - -\begin{lemma}\label{lem:measure_sum_le_sum_le'} - \uses{def:subGaussian} - \leanok - \lean{ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_sum_le'} -Let $X_1, \ldots, X_n$ be random variables such that $X_i - P[X_i]$ is $\sigma_{X,i}^2$-sub-Gaussian for $i \in [n]$. -Let $Y_1, \ldots, Y_m$ be random variables such that $Y_i - P[Y_i]$ is $\sigma_{Y,i}^2$-sub-Gaussian for $i \in [m]$. -Suppose further that the vectors $X$ and $Y$ are independent and that $\sum_{i = 1}^m P[Y_i] \le \sum_{i = 1}^n P[X_i]$. -Then -\begin{align*} - P\left(\sum_{i=1}^m Y_i \ge \sum_{i=1}^n X_i\right) - &\le \exp\left(- \frac{\left(\sum_{i = 1}^n P[X_i] - \sum_{i=1}^m P[Y_i]\right)^2}{2 \sum_{i=1}^n (\sigma_{X,i}^2 + \sigma_{Y,i}^2)}\right) - \: . -\end{align*} -\end{lemma} - -\begin{proof}\leanok - \uses{lem:subGaussian_add_of_indepFun, lem:hoeffding_one} - -\end{proof} - - - - -\section{Concentration of the sums of rewards in bandit models} - - -% TODO: this was removed, adapt the blueprint -\begin{lemma}\label{lem:AM.identDistrib_pullCount_prod_sumRewards} - \uses{def:arrayMeasure,def:AM.history,def:algorithm,def:sumRewards,def:pullCount} -In the array model, for $t \in \mathbb{N}$, the random variable $(N_{t,a}, S_{t, a})_{a \in \mathcal{A}}$ has the same distribution as $(N_{t,a}, \sum_{s=0}^{N_{t,a}-1} \omega_{2, s, a})_{a \in \mathcal{A}}$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:AM.history,lem:stepsUntil_basic,thm:ionescu-tulcea,def:algFunction,lem:AM.measurable_hist,def:rewardByCount,lem:pullCount_basic,def:stepsUntil,lem:sum_rewardByCount} - -\end{proof} - - -\begin{lemma}\label{lem:AM.identDistrib_sum_range_snd} - \uses{def:arrayMeasure,thm:ionescu-tulcea} - \leanok - \lean{Bandits.ArrayModel.identDistrib_sum_range_snd} -In the array model, for $k \in \mathbb{N}$, the random variable $\sum_{s=0}^{k-1} \omega_{2, s, a}$ has the same distribution as a sum of $k$ i.i.d. random variables with law $\nu(a)$. -\end{lemma} - -\begin{proof}\leanok -By definition of $P_{\mathcal{A}}$ (Definition~\ref{def:arrayMeasure}). -\end{proof} - - -\begin{lemma}\label{lem:prob_pullCount_prod_sumRewards_mem_le} - \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea,def:sumRewards,def:pullCount,def:stationaryEnv,def:IsAlgEnvSeq} - \leanok - \lean{Bandits.ArrayModel.prob_pullCount_prod_sumRewards_mem_le, Bandits.prob_pullCount_prod_sumRewards_mem_le} -In the array model, for $t \in \mathbb{N}$, $a \in \mathcal{A}$, and a measurable set $B \subseteq \mathbb{N} \times \mathbb{R}$, -\begin{align*} - P_{\mathcal{A}}\left((N_{t,a}, S_{t, a}) \in B\right) - &\le \sum_{k < t, \exists r, (k, r) \in B} \nu(a)^{\otimes \mathbb{N}} \left(\sum_{s=0}^{k-1} \omega_{s} \in \{x \mid \exists n, (n, x) \in B\}\right) - \: . -\end{align*} -As a consequence, this also holds for any algorithm-environment sequence. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:AM.identDistrib_sum_range_snd,lem:AM.identDistrib_pullCount_prod_sumRewards,lem:AM.measurable_hist,lem:pullCount_basic,def:arrayMeasure,def:AM.history,def:environment,thm:isAlgEnvSeq_arrayMeasure,lem:AM.measurable_hist,thm:isAlgEnvSeq_unique} - -\end{proof} - - -\begin{lemma}\label{lem:prob_sumRewards_le_sumRewards_le} - \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea,def:sumRewards,def:pullCount,def:stationaryEnv,def:IsAlgEnvSeq} - \leanok - \lean{Bandits.ArrayModel.prob_sumRewards_le_sumRewards_le, Bandits.probReal_sumRewards_le_sumRewards_le} -In the array model, -\begin{align*} - P_{\mathcal{A}}\left( N_{t, a^*} = m_1 \wedge N_{t, a} = m_2 \wedge S_{t, a^*} \le S_{t, a}\right) - &\le (\otimes_a \nu(a))^{\otimes \mathbb{N}} \left( \sum_{s=0}^{m_1-1} \omega_{s, a^*} \le \sum_{s=0}^{m_2-1} \omega_{s, a} \right) - \: . -\end{align*} -As a consequence, this also holds for any algorithm-environment sequence. -\end{lemma} - -\begin{proof}\leanok - \uses{lem:AM.identDistrib_pullCount_prod_sumRewards,lem:AM.measurable_hist,lem:pullCount_basic,def:arrayMeasure,def:AM.history,def:environment,thm:isAlgEnvSeq_arrayMeasure,lem:AM.measurable_hist,thm:isAlgEnvSeq_unique} - -\end{proof} - - - -\subsection{Sub-Gaussian rewards} - -\begin{lemma}\label{lem:probReal_sum_le_sum_streamMeasure} - \uses{thm:ionescu-tulcea,def:subGaussian,def:gap} - \leanok - \lean{Bandits.probReal_sum_le_sum_streamMeasure} -Let $\nu(a)$ be a $\sigma^2$-sub-Gaussian distribution on $\mathbb{R}$ for each arm $a \in \mathcal{A}$. -\begin{align*} - (\otimes_a \nu(a))^{\otimes \mathbb{N}} \left( \sum_{s=0}^{m-1} \omega_{s, a^*} \le \sum_{s=0}^{m-1} \omega_{s, a} \right) - &\le \exp\left( -m \frac{\Delta_a^2}{4 \sigma^2} \right) -\end{align*} -\end{lemma} - -\begin{proof}\leanok - \uses{lem:measure_sum_le_sum_le'} - -\end{proof} - - -\begin{lemma}\label{lem:prob_sum_le_sqrt_log} - \uses{thm:ionescu-tulcea,def:subGaussian} - \leanok - \lean{Bandits.prob_sum_le_sqrt_log, Bandits.prob_sum_ge_sqrt_log} -Let $\nu(a)$ be a $\sigma^2$-sub-Gaussian distribution on $\mathbb{R}$ for each arm $a \in \mathcal{A}$. -Let $c \ge 0$ be a real number and $k$ a positive natural number. -Then -\begin{align*} - \nu(a)^{\otimes \mathbb{N}} \left( \sum_{s=0}^{k-1} (\omega_{s} - \mu_a) \le - \sqrt{2 c k \sigma^2 \log(n + 1)} \right) - &\le \frac{1}{(n + 1)^{c}} - \: . -\end{align*} -The same upper bound holds for the upper tail: -\begin{align*} - \nu(a)^{\otimes \mathbb{N}} \left( \sum_{s=0}^{k-1} (\omega_{s} - \mu_a) \ge \sqrt{2 c k \sigma^2 \log(n + 1)} \right) - &\le \frac{1}{(n + 1)^{c}} - \: . -\end{align*} -\end{lemma} - -\begin{proof}\leanok - \uses{thm:hoeffding} - -\end{proof} diff --git a/blueprint/src/chapters/etc.tex b/blueprint/src/chapters/etc.tex deleted file mode 100644 index 0525c179..00000000 --- a/blueprint/src/chapters/etc.tex +++ /dev/null @@ -1,161 +0,0 @@ -\chapter{Bandit algorithms} - -\section{Round-Robin} - -This is not an interesting bandit algorithm per se, but it is used as a subroutine in other algorithms and can be a simple baseline. -This algorithm simply cycles through the arms in order. - -\begin{definition}\label{def:roundRobinAlgorithm} - \uses{def:detAlgorithm,def:algorithm} - \leanok - \lean{Learning.RoundRobin.nextAction, Learning.roundRobinAlgorithm} -The Round-Robin algorithm is defined as follows: at time $t \in \mathbb{N}$, $A_t = t \mod K$. -\end{definition} - - -\begin{lemma}\label{lem:pullCount_roundRobinAlgorithm} - \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:pullCount,def:roundRobinAlgorithm} - \leanok - \lean{Learning.RoundRobin.pullCount_mul} -For the Round-Robin algorithm, for any arm $a \in [K]$, at time $Km$ we have -\begin{align*} - N_{Km,a} - &= m - \: . -\end{align*} -\end{lemma} - -\begin{proof}\leanok - \uses{def:environment,def:detAlgorithm,def:algorithm,def:history,lem:pullCount_basic,def:roundRobinAlgorithm} - -\end{proof} - - -TODO: regret. - - - - -\section{Explore-Then-Commit} - -Note: times start at 0 to be consistent with Lean. - -Note: we will describe the algorithm by writing $A_t = ...$, but our formal bandit model needs a policy $\pi_t$ that gives the distribution of the arm to pull. What me mean is that $\pi_t$ is a Dirac distribution at that arm. - -\begin{definition}[Explore-Then-Commit algorithm]\label{def:etcAlgorithm} - \uses{def:detAlgorithm,def:algorithm} - \leanok - \lean{Bandits.ETC.nextArm, Bandits.etcAlgorithm} -The Explore-Then-Commit (ETC) algorithm with parameter $m \in \mathbb{N}$ is defined as follows: -\begin{enumerate} - \item for $t < Km$, $A_t = t \mod K$ (pull each arm $m$ times), - \item compute $\hat{A}_m^* = \arg\max_{a \in [K]} \hat{\mu}_a$, where $\hat{\mu}_a = \frac{1}{m} \sum_{t=0}^{Km-1} \mathbb{I}(A_t = a) X_t$ is the empirical mean of the rewards for arm $a$, - \item for $t \ge Km$, $A_t = \hat{A}_m^*$ (pull the empirical best arm). -\end{enumerate} -\end{definition} - - -\begin{lemma}\label{lem:ETC.isAlgEnvSeqUntil_roundRobinAlgorithm} - \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:etcAlgorithm,def:roundRobinAlgorithm} - \leanok - \lean{Bandits.ETC.isAlgEnvSeqUntil_roundRobinAlgorithm} -An algorithm-environment sequence for the Explore-Then-Commit algorithm with parameter $m$ is an algorithm-environment sequence for the Round-Robin algorithm until time $Km - 1$. -That is, ETC plays the same as Round-Robin until time $Km - 1$. -\end{lemma} - -\begin{proof} - \leanok - -\end{proof} - - -\begin{lemma}\label{lem:pullCount_etcAlgorithm} - \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:pullCount,def:etcAlgorithm} - \leanok - \lean{Bandits.ETC.pullCount_of_ge} -For the Explore-Then-Commit algorithm with parameter $m$, for any arm $a \in [K]$ and any time $t \ge Km$, we have -\begin{align*} - N_{t,a} - &= m + (t - Km) \mathbb{I}\{\hat{A}_m^* = a\} - \: . -\end{align*} -\end{lemma} - -\begin{proof}\leanok - \uses{def:environment,def:detAlgorithm,def:algorithm,def:history,lem:pullCount_basic,def:etcAlgorithm,lem:pullCount_roundRobinAlgorithm,lem:ETC.isAlgEnvSeqUntil_roundRobinAlgorithm} - -\end{proof} - - -\begin{lemma}\label{lem:sumRewards_bestArm_le_of_arm_mul_eq} - \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:sumRewards,def:etcAlgorithm} - \leanok - \lean{Bandits.ETC.sumRewards_bestArm_le_of_arm_mul_eq} -If $\hat{A}_m^* = a$, then we have $S_{Km, a^*} \le S_{Km, a}$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:environment,def:detAlgorithm,def:algorithm,def:history,def:pullCount,def:empMean,def:etcAlgorithm} - -\end{proof} - - -\begin{lemma}\label{lem:prob_etc_error_le_exp} - \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:subGaussian,def:gap,def:etcAlgorithm} - \leanok - \lean{Bandits.ETC.prob_arm_mul_eq_le} -Suppose that $\nu(a)$ is $\sigma^2$-sub-Gaussian for all arms $a \in [K]$. -Then for the Explore-Then-Commit algorithm with parameter $m$, for any arm $a \in [K]$ with $\Delta_a > 0$, we have $P(\hat{A}_m^* = a) \le \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right)$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:environment,lem:probReal_sum_le_sum_streamMeasure,lem:prob_sumRewards_le_sumRewards_le,def:detAlgorithm,def:algorithm,thm:ionescu-tulcea,def:sumRewards,def:history,lem:sumRewards_bestArm_le_of_arm_mul_eq,def:pullCount,def:etcAlgorithm} -By Lemma~\ref{lem:sumRewards_bestArm_le_of_arm_mul_eq}, -\begin{align*} - P(\hat{A}_m^* = a) - &\le P(S_{Km, a} \ge S_{Km, a^*}) - \: . -\end{align*} -By Lemma~\ref{lem:prob_sumRewards_le_sumRewards_le}, and then the concentration inequality of Lemma~\ref{lem:probReal_sum_le_sum_streamMeasure} we have -\begin{align*} - P\left(S_{Km, a^*} \le S_{Km, a}\right) - &\le (\otimes_a \nu(a))^{\otimes \mathbb{N}} \left( \sum_{s=0}^{m-1} \omega_{s, a^*} \le \sum_{s=0}^{m-1} \omega_{s, a} \right) - \\ - &\le \exp\left( -m \frac{\Delta_a^2}{4 \sigma^2} \right) - \: . -\end{align*} -\end{proof} - - -\begin{theorem}\label{thm:regret_etc_le} - \uses{def:stationaryEnv,def:regret,def:IsAlgEnvSeq,def:subGaussian,def:gap,def:etcAlgorithm} - \leanok - \lean{Bandits.ETC.regret_le} -Suppose that $\nu(a)$ is $\sigma^2$-sub-Gaussian for all arms $a \in [K]$. -Then for the Explore-Then-Commit algorithm with parameter $m$, the expected regret after $T$ pulls with $T \ge Km$ is bounded by -\begin{align*} - P[R_T] - &\le m \sum_{a=1}^K \Delta_a + (T - Km) \sum_{a=1}^K \Delta_a \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right) - \: . -\end{align*} -\end{theorem} - -\begin{proof}\leanok - \uses{lem:pullCount_etcAlgorithm,def:environment,def:algorithm,cor:integral_regret_eq_sum_mul,lem:prob_etc_error_le_exp,lem:pullCount_basic,def:pullCount} -By Lemma~\ref{lem:regret_eq_sum_pullCount_mul_gap}, we have $P[R_T] = \sum_{a=1}^K P\left[N_{T,a}\right] \Delta_a$~. -It thus suffices to bound $P[N_{T,a}]$ for each arm $a$ with $\Delta_a > 0$. -It suffices to prove that -\begin{align*} - P[N_{T,a}] - &\le m + (T - Km) \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right) - \: . -\end{align*} -By Lemma~\ref{lem:pullCount_etcAlgorithm}, -\begin{align*} - N_{T,a} - &= m + (T - Km) \mathbb{I}\{\hat{A}_m^* = a\} - \: . -\end{align*} -It thus suffices to prove the inequality $P(\hat{A}_m^* = a) \le \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right)$ for $\Delta_a > 0$. -This is done in Lemma~\ref{lem:prob_etc_error_le_exp}. -\end{proof} diff --git a/blueprint/src/chapters/intro.tex b/blueprint/src/chapters/intro.tex deleted file mode 100644 index 46a51908..00000000 --- a/blueprint/src/chapters/intro.tex +++ /dev/null @@ -1,27 +0,0 @@ -\chapter{Introduction} - -A bandit algorithm sequentially chooses actions and then observes rewards, whose distribution depends on the action chosen. -The algorithm does not know the distribution of the rewards and sees only a reward from the chosen action at any given time. -A key part of the interaction is that the algorithm can choose the next action based on all the previous actions and rewards. -The goal of the algorithm is typically to maximize the cumulative reward over time. -The researcher studying bandit algorithms is interested in the performance of the algorithm, which is measured by the ``regret'' $R_T$ after choosing $T$ actions, that is the difference between the cumulative reward of always playing the best action and the cumulative reward of the algorithm. -A theoretical guarantee will be of the form $\mathbb{E}[R_T] \le f(T)$ for some function $f$. -Here the expectation is taken over the randomness of the algorithm and the rewards. -In parallel to the theoretical study, the researcher may also be interested in the practical performance of the algorithm, which is usually measured by the average regret over several runs of the algorithm with rewards sampled from standard probability distributions. - -From that description, we highlight three key components of research work on bandit algorithms: -\begin{enumerate} - \item A bandit algorithm is both a subject of theoretical study and a practical tool, that we should be able to implement and run, - \item the bandit model defines a probability space, on which we want to take expectations, and the theoretical study deals with random variables on that space using tools like concentration inequalities, - \item for the experimental part, we need to be able to sample rewards from a range of probability distributions. -\end{enumerate} - -\section{Notations} - -$P(E)$ is the probability of event $E$ under the probability distribution $P$. - -$P[X]$ is the expectation of random variable $X$. - -$P[X \mid Y]$ is the conditional expectation of random variable $X$ given random variable $Y$. - -$P(X \mid Y)$ is the conditional distribution of random variable $X$ given random variable $Y$. diff --git a/blueprint/src/chapters/practicalAlgorithms.tex b/blueprint/src/chapters/practicalAlgorithms.tex deleted file mode 100644 index 6b59808d..00000000 --- a/blueprint/src/chapters/practicalAlgorithms.tex +++ /dev/null @@ -1,32 +0,0 @@ -\chapter{Practical Algorithms} - -The algorithms presented in the previous chapters are theoretical algorithms, in the very basic sense that they perform operations on real numbers to decide what they will sample, and those numbers are not representable in a computer. In practice, we need to use floating point numbers (or bounded integers or rationals), both for the algorithm and for the rewards that are sampled from the environment. - -We will want to perform experiments about the algorithms for which we have theoretical guarantees, and that means using an implementation of the algorithms that can actually run on a computer. -However if we use \texttt{float} in the specification of the algorithms, we won't be able to prove anything, because those numbers lack any good algebraic properties. - -Our strategy to resolve that conflict is to describe first the algorithm as a function of real numbers, and then automatically generate a version of the algorithm that uses floating point numbers, by using a translation tactic (similar to \texttt{to\_additive}). -The result is that we have only one hand-written algorithm, and even though the theorems don't directly apply to the floating point version, we are assured that the only difference between the experimental and theoretical algorithms is the result of the translation tactic. -This is in stark contrast with the situation in the literature, where the theoretical algorithm is specified in pseudo-code in LaTeX and the experiments are done on a separately written implementation, typically in Python. The experimental version may or may not be also implementing a series of tricks or optimizations of constants. - -TODO: describe the translation tactic. It should basically be like \texttt{to\_additive}. - - -\paragraph{Alternative strategy: atomic typeclasses} - -The ETC algorithm makes sense for any reward type on which we can define addition and the maximum. -As written, it also requires division by natural numbers but we could equivalently compare sums of rewards instead of empirical means. The UCB algorithm also requires multiplication, a square root and a logarithm. - -We can write the algorithm under typeclasses stating that those operations exist. Those typeclasses would be satisfied by both the real numbers and floating point numbers. -That way, the algorithm is only written once. -We would still only get theorems about the real number version because proving theorems will actually require algebraic properties on the reward type, but we don't need to write a translation tactic. - - -\paragraph{Error sensitivity analysis} - -A more theoretically satisfying but more involved method to link the Float and Real worlds is to assume in the theoretical analysis that each of the operations performed by the algorithm is imprecise: it is only supposed to give the expected result up to a specified error margin. -Then we could prove regret bounds on the algorithm that apply under that imprecise assumption. - -Finally, we need to prove such error bounds for Float operations. The bounds might depend on the magnitude of the numbers involved. - -This method would give theoretical guarantees about the algorithm that is actually running, but the theoretical analysis would depart from the standard literature on bandits and would be more tedious because of the need to track error terms. diff --git a/blueprint/src/chapters/sampling.tex b/blueprint/src/chapters/sampling.tex deleted file mode 100644 index d6a7fe56..00000000 --- a/blueprint/src/chapters/sampling.tex +++ /dev/null @@ -1 +0,0 @@ -\chapter{Sampling} diff --git a/blueprint/src/chapters/ucb.tex b/blueprint/src/chapters/ucb.tex deleted file mode 100644 index 1290d450..00000000 --- a/blueprint/src/chapters/ucb.tex +++ /dev/null @@ -1,185 +0,0 @@ -\section{UCB} - -\begin{definition}[UCB algorithm]\label{def:ucbAlgorithm} - \uses{def:detAlgorithm,def:algorithm} - \leanok - \lean{Bandits.UCB.nextArm, Bandits.ucbAlgorithm} -The UCB algorithm with parameter $c \in \mathbb{R}_+$ is defined as follows: -\begin{enumerate} - \item for $t < K$, $A_t = t \mod K$ (pull each arm once), - \item for $t \ge K$, $A_t = \arg\max_{a \in [K]} \left( \hat{\mu}_{t,a} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,a}}} \right)$, where $\hat{\mu}_{t,a} = \frac{1}{N_{t,a}} \sum_{s=0}^{t-1} \mathbb{I}(A_s = a) X_s$ is the empirical mean of the rewards for arm $a$. -\end{enumerate} -\end{definition} - -Note: the argmax in the second step is chosen in a measurable way. - - -\begin{lemma}\label{lem:UCB.isAlgEnvSeqUntil_roundRobinAlgorithm} - \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:ucbAlgorithm,def:roundRobinAlgorithm} - \leanok - \lean{Bandits.UCB.isAlgEnvSeqUntil_roundRobinAlgorithm} -An algorithm-environment sequence for the UCB algorithm is an algorithm-environment sequence for the Round-Robin algorithm until time $K - 1$. -That is, UCB plays the same as Round-Robin until time $K - 1$. -\end{lemma} - -\begin{proof} - \leanok - -\end{proof} - - -\begin{lemma}\label{lem:ucbIndex_le_ucbIndex_arm} - \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:ucbAlgorithm,def:pullCount,def:empMean} - \leanok - \lean{Bandits.UCB.ucbIndex_le_ucbIndex_arm} -For the UCB algorithm, for all time $t \ge K$ and arm $a \in [K]$, we have -\begin{align*} - \hat{\mu}_{t,a} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,a}}} - &\le \hat{\mu}_{t,A_t} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,A_t}}} - \: . -\end{align*} -\end{lemma} - -\begin{proof}\leanok - \uses{def:environment,def:detAlgorithm,def:algorithm,def:sumRewards,def:ucbAlgorithm,def:history} -By definition of the algorithm. -\end{proof} - - -\begin{lemma}\label{lem:gap_arm_le_two_mul_ucbWidth} - \uses{def:pullCount,def:gap,def:empMean,def:pullCount,def:gap,def:empMean} - \leanok - \lean{Bandits.UCB.gap_arm_le_two_mul_ucbWidth, Bandits.UCB.pullCount_arm_le} -Suppose that we have the 3 following conditions: -\begin{enumerate} - \item $\mu^* \le \hat{\mu}_{t, a^*} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,a^*}}}$, - \item $\hat{\mu}_{t,A_t} - \sqrt{\frac{2 c \log(t + 1)}{N_{t,A_t}}} \le \mu_{A_t}$, - \item $\hat{\mu}_{t, a^*} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,a^*}}} \le \hat{\mu}_{t,A_t} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,A_t}}}$. -\end{enumerate} -Then if $N_{t,A_t} > 0$ we have -\begin{align*} - \Delta_{A_t} - &\le 2 \sqrt{\frac{2 c \log(t + 1)}{N_{t,A_t}}} - \: . -\end{align*} -And in turn, if $\Delta_{A_t} > 0$ we get -\begin{align*} - N_{t,A_t} - &\le \frac{8 c \log(t + 1)}{\Delta_{A_t}^2} - \: . -\end{align*} - -Note that the third condition is always satisfied for UCB by Lemma~\ref{lem:ucbIndex_le_ucbIndex_arm}, but this lemma, as stated, is independent of the UCB algorithm. -\end{lemma} - -\begin{proof}\leanok - -\end{proof} - - -\begin{lemma}\label{lem:prob_ucbIndex_le} - \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:subGaussian,def:ucbAlgorithm,def:pullCount,def:empMean} - \leanok - \lean{Bandits.UCB.prob_ucbIndex_le, Bandits.UCB.prob_ucbIndex_ge} -Suppose that $\nu(a)$ is $\sigma^2$-sub-Gaussian for all arms $a \in [K]$. -Let $c \ge 0$ be a real number. -Then for any time $n \in \mathbb{N}$ and any arm $a \in [K]$, we have -\begin{align*} - P\left(0 < N_{n, a} \ \wedge \ \hat{\mu}_{n, a} + \sqrt{\frac{2 c \sigma^2 \log(n + 1)}{N_{n,a}}} \le \mu_a\right) - &\le \frac{1}{(n + 1)^{c - 1}} - \: . -\end{align*} -And also, -\begin{align*} - P\left(0 < N_{n, a} \ \wedge \ \hat{\mu}_{n, a} - \sqrt{\frac{2 c \sigma^2 \log(n + 1)}{N_{n,a}}} \ge \mu_a\right) - &\le \frac{1}{(n + 1)^{c - 1}} - \: . -\end{align*} -\end{lemma} - -\begin{proof}\leanok - \uses{lem:prob_sum_le_sqrt_log,thm:ionescu-tulcea,lem:prob_pullCount_prod_sumRewards_mem_le} - -\end{proof} - - -\begin{lemma}\label{lem:pullCount_le_add_three} - \uses{def:pullCount,def:empMean,def:stationaryEnv,def:IsAlgEnvSeq,def:ucbAlgorithm} - \leanok - \lean{Bandits.UCB.pullCount_le_add_three, Bandits.UCB.pullCount_le_add_three_ae} -For $C$ a natural number, for any time $n \in \mathbb{N}$ and any arm $a \in [K]$, we have -\begin{align*} - N_{n,a} - &\le C + 1 - \\&\quad + - \sum_{s=1}^{n-1} \mathbb{I}\{A_s = a \ \wedge \ C < N_{s,a} \ \wedge \ - \mu^* \le \hat{\mu}_{s, a^*} + \sqrt{\frac{2 c \sigma^2 \log(s + 1)}{N_{s,a^*}}} \ \wedge \ - \hat{\mu}_{s, A_s} - \sqrt{\frac{2 c \sigma^2 \log(s + 1)}{N_{s,A_s}}} \le \mu_{A_s}\} - \\&\quad + - \sum_{s=1}^{n-1} - \mathbb{I}\{0 < N_{s, a^*} \ \wedge \ \hat{\mu}_{s, a^*} + \sqrt{\frac{2 c \sigma^2 \log(s + 1)}{N_{s,a^*}}} < - \mu^*\} - \\&\quad + - \sum_{s=1}^{n-1} - \mathbb{I}\{0 < N_{s, a} \ \wedge \ \mu_a < - \hat{\mu}_{s, a} - \sqrt{\frac{2 c \sigma^2 \log(s + 1)}{N_{s,a}}}\} -\end{align*} -\end{lemma} - -\begin{proof}\leanok - \uses{def:environment,def:detAlgorithm,def:algorithm,def:ucbAlgorithm,def:history,lem:pullCount_basic} - -\end{proof} - - -\begin{lemma}\label{lem:some_sum_eq_zero} - \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:ucbAlgorithm,def:pullCount,def:gap,def:empMean} - \leanok - \lean{Bandits.UCB.some_sum_eq_zero} -For the UCB algorithm with parameter $c \sigma^2 \ge 0$, for any time $n \in \mathbb{N}$ and any arm $a \in [K]$ with positive gap, the first sum in Lemma~\ref{lem:pullCount_le_add_three} is equal to zero for positive $C$ such that $C \ge \frac{8 c \sigma^2 \log(n + 1)}{\Delta_a^2}$. -\end{lemma} - -\begin{proof}\leanok - \uses{def:environment,def:detAlgorithm,def:algorithm,def:ucbAlgorithm,lem:ucbIndex_le_ucbIndex_arm,def:history,lem:pullCount_basic,lem:gap_arm_le_two_mul_ucbWidth} - -\end{proof} - - -\begin{lemma}\label{lem:expectation_pullCount_le} - \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:subGaussian,def:ucbAlgorithm,def:pullCount,def:gap} - \leanok - \lean{Bandits.UCB.expectation_pullCount_le} -Suppose that $\nu(a)$ is $\sigma^2$-sub-Gaussian for all arms $a \in [K]$. -For the UCB algorithm with parameter $c \sigma^2 > 0$, for any time $n \in \mathbb{N}$ and any arm $a \in [K]$ with positive gap, we have -\begin{align*} - P[N_{n,a}] - &\le \frac{8 c \sigma^2 \log(n + 1)}{\Delta_a^2} + 2 + 2 \sum_{s=0}^{n-1} \frac{1}{(s + 1)^{c - 1}} - \: . -\end{align*} -\end{lemma} - -\begin{proof}\leanok - \uses{def:environment,def:algorithm,def:sumRewards,lem:some_sum_eq_zero,lem:prob_ucbIndex_le,lem:pullCount_basic,def:empMean,lem:pullCount_le_add_three} - -\end{proof} - - -\begin{lemma}\label{lem:ucb_regret_le} - \uses{def:stationaryEnv,def:regret,def:IsAlgEnvSeq,def:subGaussian,def:ucbAlgorithm,def:gap} - \leanok - \lean{Bandits.UCB.regret_le} -Suppose that $\nu(a)$ is $\sigma^2$-sub-Gaussian for all arms $a \in [K]$. -For the UCB algorithm with parameter $c \sigma^2 > 0$, for any time $n \in \mathbb{N}$, we have -\begin{align*} - P[R_n] - &\le \sum_{a : \Delta_a > 0} \left(\frac{8 c \sigma^2 \log(n + 1)}{\Delta_a} + 2 \Delta_a\left(1 + \sum_{s=0}^{n-1} \frac{1}{(s + 1)^{c - 1}}\right)\right) - \: . -\end{align*} -\end{lemma} - -\begin{proof}\leanok - \uses{def:environment,def:algorithm,cor:integral_regret_eq_sum_mul,lem:pullCount_basic,lem:expectation_pullCount_le,def:pullCount} - -\end{proof} - -TODO: for $c > 2$, the sum converges to a constant, so we get a logarithmic regret bound. diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex deleted file mode 100644 index 79e62c88..00000000 --- a/blueprint/src/content.tex +++ /dev/null @@ -1,22 +0,0 @@ -% In this file you should put the actual content of the blueprint. -% It will be used both by the web and the print version. -% It should *not* include the \begin{document} -% -% If you want to split the blueprint content into several files then -% the current file can be a simple sequence of \input. Otherwise It -% can start with a \section or \chapter for instance. - -\input{chapters/intro.tex} -\input{chapters/algorithm.tex} -\input{chapters/bandit.tex} -\input{chapters/concentration.tex} -\input{chapters/etc.tex} -\input{chapters/ucb.tex} -\input{chapters/practicalAlgorithms.tex} - -\bibliographystyle{amsalpha} -\bibliography{biblio} - -\appendix - -\input{appendix/conditional_independence.tex} diff --git a/blueprint/src/extra_styles.css b/blueprint/src/extra_styles.css deleted file mode 100644 index b96c7767..00000000 --- a/blueprint/src/extra_styles.css +++ /dev/null @@ -1,25 +0,0 @@ -/* This file contains CSS tweaks for this blueprint. - * As an example, we included CSS rules that put - * a vertical line on the left of theorem statements - * and proofs. - * */ - -div.theorem_thmcontent { - border-left: .15rem solid black; -} - -div.proposition_thmcontent { - border-left: .15rem solid black; -} - -div.lemma_thmcontent { - border-left: .1rem solid black; -} - -div.corollary_thmcontent { - border-left: .1rem solid black; -} - -div.proof_content { - border-left: .08rem solid grey; -} diff --git a/blueprint/src/latexmkrc b/blueprint/src/latexmkrc deleted file mode 100644 index 38d59630..00000000 --- a/blueprint/src/latexmkrc +++ /dev/null @@ -1,5 +0,0 @@ -# This file configures the latexmk command you can use to compile -# the pdf version of the blueprint -$pdf_mode = 1; -$pdflatex = 'xelatex -synctex=1'; -@default_files = ('print.tex'); \ No newline at end of file diff --git a/blueprint/src/macros/common.tex b/blueprint/src/macros/common.tex deleted file mode 100644 index 76c6969c..00000000 --- a/blueprint/src/macros/common.tex +++ /dev/null @@ -1,21 +0,0 @@ -% In this file you should put all LaTeX macros and settings to be used both by -% the pdf version and the web version. -% This should be most of your macros. - -% The theorem-like environments defined below are those that appear by default -% in the dependency graph. See the README of leanblueprint if you need help to -% customize this. -% The configuration below use the theorem counter for all those environments -% (this is what the [theorem] arguments mean) and never resets it. -% If you want for instance to number them within chapters then you can add -% [chapter] at the end of the next line. -\newtheorem{theorem}{Theorem}[chapter] -\newtheorem{proposition}[theorem]{Proposition} -\newtheorem{lemma}[theorem]{Lemma} -\newtheorem{corollary}[theorem]{Corollary} - -\theoremstyle{definition} -\newtheorem{definition}[theorem]{Definition} -\newtheorem{remark}[theorem]{Remark} - -\newcommand{\ind}{\perp\!\!\!\!\perp} diff --git a/blueprint/src/macros/print.tex b/blueprint/src/macros/print.tex deleted file mode 100644 index 78708343..00000000 --- a/blueprint/src/macros/print.tex +++ /dev/null @@ -1,29 +0,0 @@ -% In this file you should put macros to be used only by -% the printed version. Of course they should have a corresponding -% version in macros/web.tex. -% Typically the printed version could have more fancy decorations. -% This should be a very short file. -% -% This file starts with dummy macros that ensure the pdf -% compiler will ignore macros provided by plasTeX that make -% sense only for the web version, such as dependency graph -% macros. - - -% Dummy macros that make sense only for web version. -\newcommand{\lean}[1]{} -\newcommand{\discussion}[1]{} -\newcommand{\leanok}{} -\newcommand{\mathlibok}{} -\newcommand{\notready}{} -% Make sure that arguments of \uses and \proves are real labels, by using invisible refs: -% latex prints a warning if the label is not defined, but nothing is shown in the pdf file. -% It uses LaTeX3 programming, this is why we use the expl3 package. -\ExplSyntaxOn -\NewDocumentCommand{\uses}{m} - {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}% - \ignorespaces} -\NewDocumentCommand{\proves}{m} - {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}% - \ignorespaces} -\ExplSyntaxOff diff --git a/blueprint/src/macros/web.tex b/blueprint/src/macros/web.tex deleted file mode 100644 index ceee9755..00000000 --- a/blueprint/src/macros/web.tex +++ /dev/null @@ -1,5 +0,0 @@ -% In this file you should put macros to be used only by -% the web version. Of course they should have a corresponding -% version in macros/print.tex. -% Typically the printed version could have more fancy decorations. -% This will probably be a very short file. \ No newline at end of file diff --git a/blueprint/src/plastex.cfg b/blueprint/src/plastex.cfg deleted file mode 100644 index de3dbae2..00000000 --- a/blueprint/src/plastex.cfg +++ /dev/null @@ -1,17 +0,0 @@ -[general] -renderer=HTML5 -copy-theme-extras=yes -plugins=plastexdepgraph plastexshowmore leanblueprint - -[document] -toc-depth=3 -toc-non-files=True - -[files] -directory=../web/ -split-level= 0 - -[html5] -localtoc-level=0 -extra-css=extra_styles.css -mathjax-dollars=False \ No newline at end of file diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex deleted file mode 100644 index 2ecf7ed1..00000000 --- a/blueprint/src/print.tex +++ /dev/null @@ -1,33 +0,0 @@ -% This file makes a printable version of the blueprint -% It should include all the \usepackage needed for the pdf version. -% The template version assume you want to use a modern TeX compiler -% such as xeLaTeX or luaLaTeX including support for unicode -% and Latin Modern Math font with standard bugfixes applied. -% It also uses expl3 in order to support macros related to the dependency graph. -% It also includes standard AMS packages (and their improved version -% mathtools) as well as support for links with a sober decoration -% (no ugly rectangles around links). -% It is otherwise a very minimal preamble (you should probably at least -% add cleveref and tikz-cd). - -\documentclass[a4paper]{report} - -\usepackage{geometry} - -\usepackage{expl3} - -\usepackage{amssymb, amsthm, mathtools} -\usepackage[unicode,colorlinks=true,linkcolor=blue,urlcolor=magenta, citecolor=blue]{hyperref} - -\usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math} - -\input{macros/common} -\input{macros/print} - -\title{Lean Machine Learning\\ \Large{A Lean package for machine learning algorithms}} -\author{Rémy Degenne, Paulo Rauber} - -\begin{document} -\maketitle -\input{content} -\end{document} diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex deleted file mode 100644 index 15f39f04..00000000 --- a/blueprint/src/web.tex +++ /dev/null @@ -1,34 +0,0 @@ -% This file makes a web version of the blueprint -% It should include all the \usepackage needed for this version. -% The template includes standard AMS packages. -% It is otherwise a very minimal preamble (you should probably at least -% add cleveref and tikz-cd). - -\documentclass{report} - -\usepackage{amssymb, amsthm, amsmath} -\usepackage{hyperref} -\usepackage[showmore, dep_graph]{blueprint} - - -\input{macros/common} -\input{macros/web} - -\graphcolor{mathlib}{purple}{The statement of this result is in Mathlib} - -\home{https://leanmachinelearning.github.io} -\github{https://github.com/LeanMachineLearning/LML} -\dochome{https://leanmachinelearning.github.io/LML/docs} - -\title{Lean Machine Learning} -\author{Rémy Degenne, Paulo Rauber} - -\begin{document} -\maketitle - -\begin{center} - \Large{A Lean package for machine learning algorithms} -\end{center} - -\input{content} -\end{document} diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml deleted file mode 100644 index cddfcc16..00000000 --- a/docbuild/lakefile.toml +++ /dev/null @@ -1,15 +0,0 @@ -name = "docbuild" -reservoir = false -version = "0.1.0" -packagesDir = "../.lake/packages" - -[[require]] -name = "LeanMachineLearning" -path = "../" - -[[require]] -scope = "leanprover" -name = "doc-gen4" -# If you are developing against a release candidate or a stable version `v4.x`, replace `main` below by `v4.x`. -# If you do not use `main` keep in mind to update this field as you update your Lean version. -rev = "main" diff --git a/scripts/build_blueprint.sh b/scripts/build_blueprint.sh deleted file mode 100755 index 3b5213c1..00000000 --- a/scripts/build_blueprint.sh +++ /dev/null @@ -1,13 +0,0 @@ -set -x -e - -cd verso_blueprint -lake exe cache get -lake build -lake exe blueprint-gen --output _out/site -mkdir -p _out/site/html-multi/static -cp static_files/* _out/site/html-multi/static -cd .. - -# Copy outputs to home_page -mkdir -p home_page/verso_blueprint -cp -r verso_blueprint/_out/site/html-multi/* home_page/verso_blueprint diff --git a/verso_blueprint/LMLBlueprint.lean b/verso_blueprint/LMLBlueprint.lean deleted file mode 100644 index df46b6c8..00000000 --- a/verso_blueprint/LMLBlueprint.lean +++ /dev/null @@ -1 +0,0 @@ -import LMLBlueprint.Blueprint diff --git a/verso_blueprint/LMLBlueprint/Blueprint.lean b/verso_blueprint/LMLBlueprint/Blueprint.lean deleted file mode 100644 index 869ff0bd..00000000 --- a/verso_blueprint/LMLBlueprint/Blueprint.lean +++ /dev/null @@ -1,31 +0,0 @@ -import Verso -import VersoManual -import VersoBlueprint -import VersoBlueprint.Commands.Graph -import VersoBlueprint.Commands.Summary -import LMLBlueprint.Chapters.Algorithm -import LMLBlueprint.Chapters.Bandit -import LMLBlueprint.Chapters.BanditAlgs -import LMLBlueprint.Chapters.Concentration -import LMLBlueprint.Chapters.Intro - -open Verso.Genre -open Verso.Genre.Manual -open Informal - -set_option verso.blueprint.foldProofs true -set_option verso.blueprint.summary.debugDiagnostics false - -#doc (Manual) "Lean Machine Learning" => - -Blueprint for the bandit parts of the [Lean Machine Learning](https://leanmachinelearning.org) library. - -{include 0 LMLBlueprint.Chapters.Intro} -{include 0 LMLBlueprint.Chapters.Algorithm} -{include 0 LMLBlueprint.Chapters.Bandit} -{include 0 LMLBlueprint.Chapters.Concentration} -{include 0 LMLBlueprint.Chapters.BanditAlgs} - -{blueprint_graph} -{blueprint_summary} -{blueprint_bibliography} diff --git a/verso_blueprint/LMLBlueprint/Chapters/Algorithm.lean b/verso_blueprint/LMLBlueprint/Chapters/Algorithm.lean deleted file mode 100644 index f8495655..00000000 --- a/verso_blueprint/LMLBlueprint/Chapters/Algorithm.lean +++ /dev/null @@ -1,492 +0,0 @@ -import Verso -import VersoManual -import VersoBlueprint -import LeanMachineLearning.SequentialLearning.Deterministic -import LeanMachineLearning.SequentialLearning.FiniteActions -import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace -import LeanMachineLearning.SequentialLearning.StationaryEnv -import LMLBlueprint.References -import LMLBlueprint.TeXPrelude - -open Verso.Genre -open Verso.Genre.Manual -open Informal - -#doc (Manual) "Iterative stochastic algorithms" => - -:::group "algorithm_environment" -Stochastic algorithms and environments -::: - -Warning: all times start at zero. - -TODO: notations - -All measurable spaces are assumed to be standard Borel. - -:::definition "algorithm" (parent := "algorithm_environment") (lean := "Learning.Algorithm") -A sequential, stochastic algorithm with actions in a measurable space $`\mathcal{A}` and observations in a measurable space $`\mathcal{R}` is described by the following data: -- for all $`t \in \mathbb{N}`, a policy $`\pi_t : (\mathcal{A} \times \mathcal{R})^{t+1} \rightsquigarrow \mathcal{A}`, a Markov kernel which gives the distribution of the action of the algorithm at time $`t+1` given the history of previous actions and observations, -- $`P_0 \in \mathcal{P}(\mathcal{A})`, a probability measure that gives the distribution of the first action. -::: - -After the algorithm takes an action, the environment generates an observation according to a Markov kernel $`\nu_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times \mathcal{A} \rightsquigarrow \mathcal{R}`. - -:::definition "environment" (parent := "algorithm_environment") (lean := "Learning.Environment") -An environment with which an algorithm interacts is described by the following data: -- for all $`t \in \mathbb{N}`, a feedback $`\nu_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times \mathcal{A} \rightsquigarrow \mathcal{R}`, a Markov kernel which gives the distribution of the observation at time $`t+1` given the history of previous pulls and observations, and the action of the algorithm at time $`t+1`, -- $`\nu'_0 \in \mathcal{A} \rightsquigarrow \mathcal{R}`, a Markov kernel that gives the distribution of the first observation given the first action. -::: - - -:::definition "detAlgorithm" (parent := "algorithm_environment") (lean := "Learning.detAlgorithm") -An algorithm ({uses "algorithm"}[]) is deterministic if its initial probability measure $`P_0` is a Dirac measure and if all its policies $`\pi_t` are deterministic kernels. -::: - - -:::definition "stationaryEnv" (parent := "algorithm_environment") (lean := "Learning.stationaryEnv") -An environment ({uses "environment"}[]) is stationary if there exists a Markov kernel $`\nu : \mathcal{A} \rightsquigarrow \mathcal{R}` such that $`\nu'_0 = \nu` and for all $`t \in \mathbb{N}`, for all $`h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}`, for all $`a \in \mathcal{A}`, $`\nu_t(h_t, a) = \nu(a)`. -::: - -TODO: possibly change the _stationary_ name. - - -Let's detail four examples of interactions between an algorithm and an environment. -- *First order optimization*. The objective of the algorithm is to find the minimum of a function $`f : \mathbb{R}^d \to \mathbb{R}`. - The action space is $`\mathcal{A} = \mathbb{R}^d` (a point on which the function will be queried) and the observation space is $`\mathcal{R} = \mathbb{R} \times \mathbb{R}^d`. - The environment is described by a function $`g : \mathbb{R}^d \to \mathbb{R} \times \mathbb{R}^d` such that for all $`x \in \mathbb{R}^d`, $`g(x) = (f(x), \nabla f(x))`. That is, the kernel $`\nu_t` is deterministic and depends only on the action: it is given by $`\nu_t(h_t, x) = \delta_{g(x)}` (the Dirac measure at $`g(x)`). - An example of algorithm is gradient descent with fixed step size $`\eta > 0`: this is a deterministic algorithm defined by $`P_0 = \delta_{x_0}` for some initial point $`x_0 \in \mathbb{R}^d` and for all $`t \in \mathbb{N}`, $`\pi_t(h_t) = \delta_{x_{t+1}}` where $`x_{t+1} = x_t - \eta \nabla g_2(x_t)`. -- *Stochastic bandits*. The action space is $`\mathcal{A} = [K]` for some $`K \in \mathbb{N}` (the set of arms) and the observation space is $`\mathcal{R} = \mathbb{R}` (the reward obtained after pulling an arm). - The kernel $`\nu_t` is stationary and depends only on the action: there are probability distributions $`(P_a)_{a \in [K]}` such that for all $`t \in \mathbb{N}`, for all $`h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}`, for all $`a \in \mathcal{A}`, $`\nu_t(h_t, a) = P_a`. -- *Adversarial bandits*. The action space is $`\mathcal{A} = [K]` for some $`K \in \mathbb{N}` (the set of arms) and the observation space is $`\mathcal{R} = \mathbb{R}` (the reward obtained after pulling an arm). - The reward kernels are usually taken to be deterministic and in an _oblivious_ adversarial bandit they depend only on the time step: there is a sequence of vectors $`(r_t)_{t \in \mathbb{N}}` in $`[0,1]^K` such that for all $`t \in \mathbb{N}`, for all $`h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}`, for all $`a \in \mathcal{A}`, $`\nu_t(h_t, a) = \delta_{r_{t,a}}` (the Dirac measure at $`r_{t,a}`). -- *Reinforcement learning in Markov decision processes*. - TODO: main feature is that $`\mathcal{R} = \mathcal{S} \times \mathbb{R}` where $`\mathcal{S}` is the state space, and the kernel $`\nu_t` depends on the last state only. - - -We will want to make global probabilistic statements about the whole sequence of actions and observations. -For example, we may want to prove that an optimization algorithm converges to the minimum of a function almost surely. -For such a statement to make sense, we need a probability space on which the whole sequence of actions and observations is defined as a random variable. - -We denote by $`P(X \mid Y)` the conditional distribution of a random variable $`X` given another random variable $`Y` under a probability measure $`P`. -When we write that $`P(X \mid Y) = \kappa`, or that $`X` has conditional distribution $`\kappa` given $`Y`, the equality should be understood as holding $`Y_* P`-almost surely. - -*Lean remark*: `HasCondDistrib` - -In the Lean implementation, we define a predicate to state those almost sure equalities of conditional distributions: `HasCondDistrib X Y k P` states that under the probability measure $`P`, the random variable $`X` has conditional distribution $`k` given the random variable $`Y` (almost surely with respect to the law of $`X`). -For convenience, the predicate also records that both random variables are almost everywhere measurable. - - -:::definition "history" (parent := "algorithm_environment") (lean := "Learning.IsAlgEnvSeq.hist, Learning.IsAlgEnvSeq.step") -For two sequences of random variables $`A : \mathbb{N} \to \Omega \to \mathcal{A}` and $`R : \mathbb{N} \to \Omega \to \mathcal{R}` (actions and observations), we call step of the interaction at time $`t` the random variable $`X_t : \Omega \to \mathcal{A} \times \mathcal{R}` defined by $`X_t(\omega) = (A_t(\omega), R_t(\omega))`. -We call history up to time $`t` the random variable $`H_t : \Omega \to (\mathcal{A} \times \mathcal{R})^{t+1}` defined by $`H_t(\omega) = (X_0(\omega), \ldots, X_t(\omega))`. -::: - - -:::definition "IsAlgEnvSeq" (parent := "algorithm_environment") (lean := "Learning.IsAlgEnvSeq") -Let $`\mathfrak{A}` be an algorithm ({uses "algorithm"}[]) and $`\mathfrak{E}` be an environment ({uses "environment"}[]). -A probability space $`(\Omega, P)` and two sequences of random variables $`A : \mathbb{N} \to \Omega \to \mathcal{A}` and $`R : \mathbb{N} \to \Omega \to \mathcal{R}` form an algorithm-environment interaction for $`\mathfrak{A}` and $`\mathfrak{E}` if the following conditions hold: -1. The law of $`A_0` is $`P_0`. -2. $`P \left( R_0 \mid A_0 \right) = \nu'_0`. -3. For all $`t \in \mathbb{N}`, $`P\left(A_{t+1} \mid A_0, R_0, \ldots, A_t, R_t \right) = \pi_t`. -4. For all $`t \in \mathbb{N}`, $`P\left(R_{t+1} \mid A_0, R_0, \ldots, A_t, R_t, A_{t+1}\right) = \nu_t`. - -Uses: {uses "history"}[] -::: - - -:::lemma_ "law_step" (parent := "algorithm_environment") (lean := "Learning.IsAlgEnvSeq.hasLaw_step_zero, Learning.IsAlgEnvSeq.hasCondDistrib_step") -In an algorithm-environment interaction $`(A, R, P)` as in {uses "IsAlgEnvSeq"}[], -- the law of the initial step $`X_0` is $`P_0 \otimes \nu'_0`, -- for all $`t \in \mathbb{N}`, $`P \left( X_{t+1} \mid H_t \right) = \pi_t \otimes \nu_t`. -::: - -:::proof "law_step" -Immediate from the properties of an algorithm-environment interaction. -::: - - -:::definition "IsAlgEnvSeq.filtration" (parent := "algorithm_environment") (lean := "Learning.IsAlgEnvSeq.filtration, Learning.IsAlgEnvSeq.filtrationAction") -For an algorithm-environment interaction $`(A, R, P)` as in {uses "IsAlgEnvSeq"}[], we denote by $`\mathcal{F}_t` the sigma-algebra generated by the history up to time $`t`: $`\mathcal{F}_t = \sigma(H_t)`. -We denote by $`\mathcal{F}^A_t` the sigma-algebra generated by the history up to time $`t-1` and the action at time $`t`: $`\mathcal{F}^A_t = \sigma(H_{t-1}, A_t)`. -::: - - -:::lemma_ "IsAlgEnvSeq.adapted" (parent := "algorithm_environment") (lean := "Learning.IsAlgEnvSeq.adapted_step, Learning.IsAlgEnvSeq.adapted_hist, Learning.IsAlgEnvSeq.adapted_action, Learning.IsAlgEnvSeq.adapted_feedback") -The history, step, action and observation processes ({uses "history"}[]) are adapted to the filtration $`(\mathcal{F}_t)_{t \in \mathbb{N}}` ({uses "IsAlgEnvSeq.filtration"}[]). -::: - -:::proof "IsAlgEnvSeq.adapted" -By definition of the filtration. -::: - - -:::theorem "isAlgEnvSeq_unique" (parent := "algorithm_environment") (lean := "Learning.isAlgEnvSeq_unique") -If $`(A, R, P)` and $`(A', R', P')` are two {uses "IsAlgEnvSeq"}[algorithm-environment interactions] for the same {uses "algorithm"}[algorithm] $`\mathfrak{A}` and {uses "environment"}[environment] $`\mathfrak{E}`, then the joint distributions of the sequences of actions and observations are equal: the law of $`(A_i, R_i)_{i \in \mathbb{N}}` under $`P` is equal to the law of $`(A'_i, R'_i)_{i \in \mathbb{N}}` under $`P'`. - -This is Proposition 4.8 in {Informal.citep lattimore2020bandit}[]. -::: - -:::proof "isAlgEnvSeq_unique" -Uses: {uses "ionescu-tulcea"}[], {uses "law_step"}[], {uses "trajMeasure"}[] -::: - - - - -# Stationary environment - -:::group "stationary_environment" -Stationary environments -::: - -Recall that in a stationary environment, there exists a Markov kernel $`\nu : \mathcal{A} \rightsquigarrow \mathcal{R}` such that $`\nu'_0 = \nu` and for all $`t \in \mathbb{N}`, for all $`h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}`, for all $`a \in \mathcal{A}`, $`\nu_t(h_t, a) = \nu(a)`. - -Let $`(A, R, P)` be an algorithm-environment interaction in a stationary environment with kernel $`\nu`. - -:::lemma_ "condDistrib_feedback_stationaryEnv" (parent := "stationary_environment") (lean := "Learning.IsAlgEnvSeq.condDistrib_feedback_stationaryEnv") -In a {uses "stationaryEnv"}[stationary environment], an {uses "IsAlgEnvSeq"}[algorithm-environment interaction] satisfies for any $`t \in \mathbb{N}`, $`P\left(R_t \mid A_t\right) = \nu`. -::: - -:::proof "condDistrib_feedback_stationaryEnv" -Uses: {uses "law_step"}[] -::: - - -::: lemma_ "condIndepFun_feedback_hist_action" (parent := "stationary_environment") (lean := "Learning.IsAlgEnvSeq.condIndepFun_feedback_hist_action") -For an {uses "IsAlgEnvSeq"}[algorithm-environment interaction] in a {uses "stationaryEnv"}[stationary environment], for any $`t \in \mathbb{N}`, the reward $`R_{t+1}` is conditionally independent of the history $`H_t` given the action $`A_{t+1}` (more succinctly, $`R_{t+1} \ind H_t \mid A_{t+1}`). -::: - -:::proof "condIndepFun_feedback_hist_action" -::: - - - -# Probability space: Ionescu-Tulcea theorem - -We saw that the distribution of the sequence of actions and observations in a suitable probability space is uniquely determined by the algorithm and the environment. -We now show that such a probability space actually exists: for any algorithm and environment, we build an algorithm-environment interaction. - -:::group "ionescu_tulcea" -Ionescu-Tulcea theorem -::: - -## Ionescu-Tulcea theorem - -If we group together the policy of the algorithm and the kernel of the environment at each time step, we get a sequence of Markov kernels $`(\kappa_t)_{t \in \mathbb{N}}`, with $`\kappa_t : (\mathcal{A} \times \mathcal{R})^{t+1} \rightsquigarrow (\mathcal{A} \times \mathcal{R})`. - - -We now abstract that situation and consider a sequence of measurable spaces $`(\Omega_t)_{t \in \mathbb{N}}`, a probability measure $`\mu` on $`\Omega_0` and a sequence of Markov kernels $`\kappa_t : \prod_{s=0}^t \Omega_s \rightsquigarrow \Omega_{t+1}`. -The Ionescu-Tulcea theorem builds a probability space from the sequence of kernels and the initial measure. - - -:::theorem "ionescu-tulcea" (parent := "ionescu_tulcea") (lean := "ProbabilityTheory.Kernel.traj") -Let $`(\Omega_t)_{t \in \mathbb{N}}` be a family of measurable spaces. Let $`(\kappa_t)_{t \in \mathbb{N}}` be a family of Markov kernels such that for any $`t`, $`\kappa_t` is a kernel from $`\prod_{i=0}^t \Omega_{i}` to $`\Omega_{t+1}`. -Then there exists a unique Markov kernel $`\xi : \Omega_0 \rightsquigarrow \prod_{i = 1}^{\infty} \Omega_{i}` such that for any $n \ge 1$, -$`\pi_{[1,n]*} \xi = \kappa_0 \otimes \ldots \otimes \kappa_{n-1}`. -Here $`\pi_{[1,n]} : \prod_{i=1}^{\infty} \Omega_i \to \prod_{i=1}^n \Omega_i` is the projection on the first $`n` coordinates. -::: - -The Ionescu-Tulcea theorem in Mathlib {Informal.citep marion2025formalization}[] actually generates kernels $`\xi_t : \prod_{s=0}^t \Omega_s \rightsquigarrow \prod_{s=0}^{\infty} \Omega_s` for any $`t`, with the property that the kernels are the identity on the first $`t+1` coordinates. - -:::definition "trajMeasure" (parent := "ionescu_tulcea") (lean := "ProbabilityTheory.Kernel.trajMeasure") -For $`\mu \in \mathcal{P}(\Omega_0)`, we call trajectory measure the probability measure $`\xi_0 \circ \mu` on $`\Omega_{\mathcal{T}} := \prod_{i=0}^{\infty} \Omega_i`. -We denote it by $`P_{\mathcal{T}}`. -The $`\mathcal{T}` subscript stands for _trajectory_. -::: - - -:::definition "IT.history" (parent := "ionescu_tulcea") (lean := "Learning.IT.hist, Learning.IT.step") -For $`t \in \mathbb{N}`, we denote by $`X_t \in \Omega_t` the random variable describing the time step $`t`, and by $`H_t \in \prod_{s=0}^t \Omega_s` the history up to time $`t`. -Formally, these are measurable functions on $`\Omega_{\mathcal{T}}`, defined by $`X_t(\omega) = \omega_t` and $`H_t(\omega) = (\omega_1, \ldots, \omega_t)`. -::: - -Note: $`(X_t)_{t \in \mathbb{N}}` is the canonical process on $`\Omega_{\mathcal{T}}`. $`H_t` is equal to $`\pi_{[0,t]}`. - - -:::definition "IT.filtration" (parent := "ionescu_tulcea") (lean := "Learning.IT.filtration") -For $`t \in \mathbb{N}`, we denote by $`\mathcal{F}_t` the sigma-algebra generated by the {uses "IT.history"}[history] up to time $`t`: $`\mathcal{F}_t = \sigma(H_t)`. -The family $`(\mathcal{F}_t)_{t \in \mathbb{N}}` is a filtration on $`\Omega_{\mathcal{T}}`. -::: - -$`(\mathcal{F}_t)_{t \in \mathbb{N}}` is the canonical filtration on $`\Omega_{\mathcal{T}}`, and is the natural filtration for the canonical process $`(X_t)_{t \in \mathbb{N}}`. - -:::lemma_ "IT.adapted_history" (parent := "ionescu_tulcea") (lean := "Learning.IT.adapted_step, Learning.IT.adapted_hist") -The random variables $`X_t` and $`H_t` ({uses "IT.history"}[]) are $`\mathcal{F}_t`-measurable. -Said differently, the processes $`(X_t)_{t \in \mathbb{N}}` and $`(H_t)_{t \in \mathbb{N}}` are adapted to the {uses "IT.filtration"}[filtration] $`(\mathcal{F}_t)_{t \in \mathbb{N}}`. -::: - - -:::lemma_ "IT.condDistrib_X_add_one" (parent := "ionescu_tulcea") (lean := "ProbabilityTheory.Kernel.condDistrib_trajMeasure") -For any $`t \in \mathbb{N}`, $`P_{\mathcal{T}}\left(X_{t+1} \mid H_t\right) = \kappa_t`. - -Uses: {uses "IT.history"}[], {uses "ionescu-tulcea"}[], {uses "trajMeasure"}[] -::: - -:::proof "IT.condDistrib_X_add_one" -This is proved through the defining property of the conditional distribution: it is the almost surely unique Markov kernel $`\eta` such that $`((H_t)_* P_{\mathcal{T}}) \otimes \eta = (H_t, X_{t+1})_*P_{\mathcal{T}}`. - -TODO: complete proof. -::: - - -:::lemma_ "IT.law_X_zero" (parent := "ionescu_tulcea") (lean := "Learning.IsAlgEnvSeq.hasLaw_step_zero") -The law of $`X_0` under $`P_{\mathcal{T}}` is $`\mu`. - -Uses: {uses "IT.history"}[], {uses "trajMeasure"}[]. -::: - - - -## Case of an algorithm-environment interaction - -We now go back to the setting of an algorithm interacting with an environment and suppose that $`\Omega_t = \mathcal{A} \times \mathcal{R}` for some measurable spaces $`\mathcal{A}` and $`\mathcal{R}`, and that for all $`t \in \mathbb{N}`, $`\kappa_t = \pi_t \otimes \nu_t` for policy kernels $`\pi_t : (\mathcal{A} \times \mathcal{R})^{t+1} \rightsquigarrow \mathcal{A}` and feedback kernels $`\nu_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times \mathcal{A} \rightsquigarrow \mathcal{R}`. -Likewise, $`\mu = P_0 \otimes \nu'_0` for a probability measure $`P_0` on $`\mathcal{A}` and a Markov kernel $`\nu'_0 : \mathcal{A} \rightsquigarrow \mathcal{R}`. -The step random variable $`X_t` takes values in $`\mathcal{A} \times \mathcal{R}`. - -:::definition "IT.actionReward" (parent := "ionescu_tulcea") (lean := "Learning.IT.action, Learning.IT.feedback") -We write $`A_t` and $`R_t` for the projections of $`X_t` ({uses "IT.history"}[]) on $`\mathcal{A}` and $`\mathcal{R}` respectively. -$`A_t` is the action taken at time $`t` and $`R_t` is the reward received at time $`t`. -Formally, $`A_t(\omega) = \omega_{t,1}` and $`R_t(\omega) = \omega_{t,2}` for $`\omega = \prod_{t=0}^{+\infty}(\omega_{t,1}, \omega_{t,2}) \in \Omega_{\mathcal{T}} = \prod_{t=0}^{+\infty} \mathcal{A} \times \mathcal{R}`. -::: - - -:::lemma_ "IT.adapted_action_feedback" (parent := "ionescu_tulcea") (lean := "Learning.IT.adapted_action, Learning.IT.adapted_feedback") -The random variables $`A_t` and $`R_t` ({uses "IT.actionReward"}[]) are $`\mathcal{F}_t`-measurable. -Said differently, the processes $`(A_t)_{t \in \mathbb{N}}` and $`(R_t)_{t \in \mathbb{N}}` are adapted to the {uses "IT.filtration"}[filtration] $`(\mathcal{F}_t)_{t \in \mathbb{N}}`. -::: - -:::proof "IT.adapted_action_feedback" -Uses: {uses "IT.adapted_history"}[]. -::: - - -We need to check that the random variables $`A_t` and $`R_t` have the expected conditional distributions. - -:::lemma_ "IT.condDistrib_A_add_one" (parent := "ionescu_tulcea") (lean := "Learning.IT.condDistrib_action") -For any $`t \in \mathbb{N}`, $`P_{\mathcal{T}}\left(A_{t+1} \mid H_t\right) = \pi_t`. - -Uses: {uses "environment"}[], {uses "algorithm"}[], {uses "ionescu-tulcea"}[], {uses "IT.actionReward"}[], {uses "trajMeasure"}[], {uses "IT.history"}[]. -::: - -:::proof "IT.condDistrib_A_add_one" -By {uses "IT.condDistrib_X_add_one"}[], $`P_{\mathcal{T}}\left(X_{t+1} \mid H_t\right) = \kappa_t = \pi_t \otimes \nu_t`. -Since $`A_{t+1}` is the projection of $`X_{t+1}` on $`\mathcal{A}`, $`P_{\mathcal{T}}\left(A_{t+1} \mid H_t\right)` is $`((H_t)_* P_{\mathcal{T}})`-almost surely equal to the projection of $`\kappa_t` on $`\mathcal{A}`, which is $`\pi_t`. -::: - - -:::lemma_ "IT.condDistrib_R_add_one" (parent := "ionescu_tulcea") (lean := "Learning.IT.condDistrib_feedback") -For any $`t \in \mathbb{N}`, $`P_{\mathcal{T}}\left(R_{t+1} \mid H_t, A_{t+1}\right) = \nu_t`. - -Uses: {uses "environment"}[], {uses "algorithm"}[], {uses "ionescu-tulcea"}[], {uses "IT.actionReward"}[], {uses "trajMeasure"}[], {uses "IT.history"}[]. -::: - -:::proof "IT.condDistrib_R_add_one" -It suffices to show that $`((H_t, A_{t+1})_* P_{\mathcal{T}}) \otimes \nu_t = (H_t, A_{t+1}, R_{t+1})_* P_{\mathcal{T}} = (H_t, X_{t+1})_* P_{\mathcal{T}}`. -By {uses "IT.condDistrib_X_add_one"}[], $`P_{\mathcal{T}}\left(X_{t+1} \mid H_t\right) = \pi_t \otimes \nu_t`. -Thus $`((H_t)_* P_{\mathcal{T}}) \otimes (\pi_t \otimes \nu_t) = (H_t, X_{t+1})_* P_{\mathcal{T}}`. - -We thus have to prove that $`((H_t)_* P_{\mathcal{T}}) \otimes (\pi_t \otimes \nu_t) = ((H_t, A_{t+1})_* P_{\mathcal{T}}) \otimes \nu_t`. - -By {uses "IT.condDistrib_A_add_one"}[], $`(H_t, A_{t+1})_* P_{\mathcal{T}} = (H_t)_* P_{\mathcal{T}} \otimes \pi_t`, and replacing this in the right-hand side gives the left-hand side (using associativity of the composition-product). -::: - - -:::lemma_ "IT.law_A_zero" (parent := "ionescu_tulcea") (lean := "Learning.IT.hasLaw_action_zero") -The law of $`A_0` under $`P_{\mathcal{T}}` is $`P_0`. - -Uses: {uses "environment"}[], {uses "algorithm"}[], {uses "IT.actionReward"}[], {uses "trajMeasure"}[]. -::: - -:::proof "IT.law_A_zero" -$`X_0` has law $`\mu = P_0 \otimes \nu'_0`. $`A_0` is the projection of $`X_0` on the first space $`\mathcal{A}` and $`\nu_0'` is Markov, so $`A_0` has law $`P_0`. - -Uses: {uses "ionescu-tulcea"}[], {uses "IT.history"}[], {uses "IT.law_X_zero"}[]. -::: - - -:::lemma_ "IT.condDistrib_R_zero" (parent := "ionescu_tulcea") (lean := "Learning.IT.condDistrib_feedback_zero") -$`P_{\mathcal{T}}\left(R_0 \mid A_0\right) = \nu'_0`. - -Uses: {uses "environment"}[], {uses "algorithm"}[], {uses "IT.actionReward"}[], {uses "trajMeasure"}[], {uses "ionescu-tulcea"}[]. -::: - -:::proof "IT.condDistrib_R_zero" -To prove almost sure equality, it is enough to prove that $`(A_{0*} P_{\mathcal{T}}) \otimes P_{\mathcal{T}}\left(R_0 \mid A_0\right) = (A_{0*} P_{\mathcal{T}}) \otimes \nu'_0`. -By definition of the conditional distribution, we have $`(A_{0*} P_{\mathcal{T}}) \otimes P_{\mathcal{T}}\left(R_0 \mid A_0\right) = (A_0, R_0)_* P_{\mathcal{T}} = X_{0*} P_{\mathcal{T}}`. -By {uses "IT.law_X_zero"}[], $`X_{0*} P_{\mathcal{T}} = \mu = P_0 \otimes \nu'_0`. -By {uses "IT.law_A_zero"}[], $`A_{0*} P_{\mathcal{T}} = P_0`. -Thus the two sides are equal. -::: - - -:::theorem "isAlgEnvSeq_trajMeasure" (parent := "ionescu_tulcea") (lean := "Learning.IT.isAlgEnvSeq_trajMeasure") -In the {uses "trajMeasure"}[probability space $`(\Omega_{\mathcal{T}}, P_{\mathcal{T}})`] constructed from an algorithm $`\mathfrak{A}` and an environment $`\mathfrak{E}` as above, the sequences of random variables $`A : \mathbb{N} \to \Omega_{\mathcal{T}} \to \mathcal{A}` and $`R : \mathbb{N} \to \Omega_{\mathcal{T}} \to \mathcal{R}` form an {uses "IsAlgEnvSeq"}[algorithm-environment interaction] for $`\mathfrak{A}` and $`\mathfrak{E}`. - -Uses: {uses "ionescu-tulcea"}[], {uses "IT.actionReward"}[]. -::: - -:::proof "isAlgEnvSeq_trajMeasure" -The four conditions of {uses "IsAlgEnvSeq"}[] are exactly the statements of {uses "IT.law_A_zero"}[], {uses "IT.condDistrib_R_zero"}[], {uses "IT.condDistrib_A_add_one"}[] and {uses "IT.condDistrib_R_add_one"}[]. -::: - - - -# Finitely many actions - -:::group "finite_actions" -Finite action space -::: - -When the number of actions is finite, it makes sense to count how many times each action was chosen up to a certain time. -We can also define the time step at which an action was chosen a certain number of times, and the value of the reward obtained when pulling an action for the $m$-th time. - -:::definition "pullCount" (parent := "finite_actions") (lean := "Learning.pullCount") -For an action $`a \in \mathcal{A}` and a time $`t \in \mathbb{N}`, we denote by $`N_{t,a}` the number of times that action $`a` has been chosen before time $`t`, that is $`N_{t,a} = \sum_{s=0}^{t-1} \mathbb{I}\{A_s = a\}`. -::: - -Note that the sum goes up to $`t-1`, so that $`N_{t,a}` counts the number of times action $`a` was chosen _before_ time $`t`. - - -*Remark: Building vs analyzing algorithms* - -When we describe an algorithm, we give the data of the policies $`\pi_t`, which are functions of the partial history up to time $`t`, in $`(\mathcal{A} \times \mathcal{R})^{t+1}`. -That means that any tool used to define a policy must be a function defined on $`(\mathcal{A} \times \mathcal{R})^{t+1}`. -For example a definition of the empirical mean of an action must be a function $`t : \mathbb{N} \to (\mathcal{A} \times \mathcal{R})^{t+1} \to \mathbb{R}`. - -When we analyze an algorithm, we work on the other hand on a probability space $`(\Omega, P)`, in which $`\Omega` could be for example $`(\mathcal{A} \times \mathcal{R})^{\mathbb{N}}`, the full history, which describes the whole sequence of actions and rewards. -As a stochastic process, the empirical mean of an action is a function $`\mathbb{N} \to (\mathcal{A} \times \mathcal{R})^{\mathbb{N}} \to \mathbb{R}`. - -Thus there are two similar but still distinct types of objects: those defined on the partial history, which are used to build algorithms, and those defined on a generic probability space (the full history in the Ionescu-Tulcea construction), which are used to analyze algorithms. - - -:::lemma_ "pullCount_basic" (parent := "finite_actions") (lean := "Learning.pullCount_zero, Learning.pullCount_mono, Learning.pullCount_add_one, Learning.pullCount_le, Learning.pullCount_congr") -We note the following basic properties of {uses "pullCount"}[$`N_{t,a}`]: -- $`N_{0,a} = 0`. -- $`N_{t,a}` is non-decreasing in $`t`. -- $`N_{t + 1, A_t} = N_{t, A_t} + 1` and for $`a \ne A_t`, $`N_{t + 1, a} = N_{t, a}`. -- $`N_{t, a} \le t`. -- If for all $`s \le t`, $`A_s(\omega) = A_s(\omega')`, then $`N_{t+1, a}(\omega) = N_{t+1, a}(\omega')`. -::: - - -:::lemma_ "predictable_pullCount" (parent := "finite_actions") (lean := "Learning.isPredictable_pullCount") -Let $`a \in \mathcal{A}`. The process {uses "pullCount"}[$`(N_{t,a})_{t \in \mathbb{N}}`] is predictable with respect to the {uses "IsAlgEnvSeq.filtration"}[filtration $`\mathcal{F}`] of the algorithm-environment interaction. -::: - -:::proof "predictable_pullCount" -Uses: {uses "history"}[], {uses "pullCount_basic"}[] -::: - - -:::definition "stepsUntil" (parent := "finite_actions") (lean := "Learning.stepsUntil") -For an action $`a \in \mathcal{A}` and a time $`n \in \mathbb{N}`, we denote by $`T_{n,a} \in \mathbb{N} \cup \{+\infty\}` the time at which action $`a` was chosen for the $`n`-th time, that is $`T_{n,a} = \min\{s \in \mathbb{N} \mid N_{s+1,a} = n\}`. -Note that $`T_{n, a}` can be infinite if the action is not chosen $`n` times. - -Uses: {uses "pullCount"}[] -::: - -By definition, $`T_{n, a}` is the hitting time of the set $`\{n\}` by the process $`t \mapsto N_{t+1,a}`, which is adapted since $`N_{t,a}` is predictable. -Equivalently, $`T_{n, a}` is the hitting time of the set $`[n, +\infty]` by that process. - - -:::lemma_ "stepsUntil_basic" (parent := "finite_actions") (lean := "Learning.stepsUntil_zero_of_ne, Learning.stepsUntil_zero_of_eq, Learning.stepsUntil_pullCount_le, Learning.stepsUntil_pullCount_eq, Learning.action_stepsUntil, Learning.pullCount_stepsUntil_add_one, Learning.pullCount_stepsUntil") -We note the following basic properties of {uses "stepsUntil"}[$`T_{n,a}`]: -- $`T_{0,a} = 0` for $`a \ne A_0`. $`T_{0,A_0} = \infty`. -- $`T_{N_{t+1, a}, a} \le t`. -- $`T_{N_{t + 1, A_t}, A_t} = t`. -- If $`T_{n, a} \ne \infty` and $`n > 0`, then $`A_{T_{n, a}} = a`. -- If $`T_{n, a} \ne \infty`, then $`N_{T_{n, a} + 1, a} = n`. -- If $`T_{n, a} \ne \infty` and $`n > 0`, then $`N_{T_{n, a}, a} = n - 1`. -- If for all $`s \le t`, $`A_s(\omega) = A_s(\omega')`, then $`T_{n, a}(\omega) = t \iff T_{n, a}(\omega') = t`. -::: - -:::proof "stepsUntil_basic" -Uses: {uses "pullCount_basic"}[] -::: - - -:::lemma_ "isStoppingTime_stepsUntil" (parent := "finite_actions") (lean := "Learning.isStoppingTime_stepsUntil") -Let $`a \in \mathcal{A}`. For any $`n > 0`, the random variable {uses "stepsUntil"}[$`T_{n,a}`] is a stopping time with respect to the {uses "IsAlgEnvSeq.filtration"}[filtration $`\mathcal{F}`]. -::: - -:::proof "isStoppingTime_stepsUntil" -A hitting time of a set by an adapted process is a stopping time. - -Uses: {uses "pullCount_basic"}[] -::: - - -Let $`\Omega' = \mathcal{R}^{\mathbb{N} \times \mathcal{A}}` and let $`\Omega = \Omega_{\mathcal{T}} \times \Omega'` (which will be an extension of the trajectory probability space once we choose a measure on $`\Omega'`). -Let $`Z_{n, a} : \Omega \to \mathcal{R}` be the projection on the coordinate indexed by $`(n,a)` in $`\Omega'`. -Extending the probability space in that way allows us to define without ambiguity the reward received when choosing an action for the $`n`-th time, even if that action is never actually chosen $`n` times. - - -:::definition "rewardByCount" (parent := "finite_actions") (lean := "Learning.rewardByCount") -We define $`Y_{n, a} = R_{T_{n,a}} \mathbb{I}\{T_{n, a} < \infty\} + Z_{n,a} \mathbb{I}\{T_{n, a} = \infty\}`, the reward received when choosing action $`a` for the $`n`-th time if {uses "stepsUntil"}[that time] is finite, and equal to $`Z_{n,a}` otherwise. -In that expression, we see $`R_{T_{n,a}}` and $`T_{n, a}` as random variables on $`\Omega` instead of $`\Omega_{\mathcal{T}}`. -::: - - -:::lemma_ "rewardByCount_pullCount" (parent := "finite_actions") (lean := "Learning.rewardByCount_pullCount_add_one_eq_reward") -$`Y_{N_{t, A_t} + 1, A_t} = R_t`. - -Uses: {uses "rewardByCount"}[], {uses "pullCount"}[] -::: - -:::proof "rewardByCount_pullCount" -This is perhaps hard to parse at first sight, but it follows directly from the definitions. -At time $t$, the action chosen is $`A_t` and we see a reward $`R_t`. -That action had already been chosen $`N_{t, A_t}` times before time $t$, so the reward $`R_t` is the reward received when choosing action $`A_t` for the $`(N_{t, A_t} + 1)`-th time, which is $`Y_{N_{t, A_t} + 1, A_t}` by definition. - -Uses: {uses "stepsUntil_basic"}[]. -::: - - - -# Scalar rewards - -TODO: change the name _reward_ to _observation_ throughout the chapter? - -We now focus on the case where the reward space is $`\mathcal{R} = \mathbb{R}`. - -:::group "scalar_rewards" -Scalar rewards -::: - -:::definition "sumRewards" (parent := "scalar_rewards") (lean := "Learning.sumRewards") -Let $`S_{t, a} = \sum_{s=0}^{t-1} R_s \mathbb{I}\{A_s = a\}` be the sum of the rewards obtained by chosing action $`a` before time $`t`. -::: - - -:::definition "empMean" (parent := "scalar_rewards") (lean := "Learning.empMean") -Let $`\hat{\mu}_{t, a} = \frac{S_{t, a}}{N_{t, a}} = \frac{1}{N_{t,a}} \sum_{s=0}^{t-1} R_s \mathbb{I}\{A_s = a\}` if $`N_{t, a} > 0`, and $`\hat{\mu}_{t, a} = 0` otherwise. -This is the empirical mean of the rewards obtained by choosing action $`a` before time $`t`. - -Uses: {uses "sumRewards"}[], {uses "pullCount"}[] -::: - -Note: in bandit papers it is common to (implicitly) define the empirical mean as $`+\infty` when the action was never chosen, but in Lean it has to be a real number, and the Lean default value for division by zero is $`0`. - - -:::lemma_ "isPredictable_sumRewards" (parent := "scalar_rewards") (lean := "Learning.IsAlgEnvSeq.isPredictable_sumRewards, Learning.IsAlgEnvSeq.isPredictable_empMean") -The processes {uses "sumRewards"}[$`(S_{t,a})_{t \in \mathbb{N}}`] and {uses "empMean"}[$`(\hat{\mu}_{t,a})_{t \in \mathbb{N}}`] are predictable with respect to the {uses "IsAlgEnvSeq.filtration"}[filtration $`\mathcal{F}`] of the algorithm-environment interaction. -::: - -:::proof "isPredictable_sumRewards" -Uses: {uses "predictable_pullCount"}[], {uses "sumRewards"}[], {uses "empMean"}[] -::: - - -The following lemma is very useful to relate the two ways of indexing the rewards: by time step and by pull count. - -:::lemma_ "sum_rewardByCount" (parent := "scalar_rewards") (lean := "Learning.sum_rewardByCount_eq_sumRewards") -The sum of the first {uses "pullCount"}[$`N_{t, a}`] rewards received when choosing action $`a` is equal to the sum of the rewards obtained by choosing action $`a` before time $`t`: -$$`\sum_{n=1}^{N_{t, a}} Y_{n, a} = S_{t,a} \: .` - -Uses: {uses "rewardByCount"}[], {uses "sumRewards"}[]. -::: - -:::proof "sum_rewardByCount" -Uses: {uses "rewardByCount_pullCount"}[]. -::: diff --git a/verso_blueprint/LMLBlueprint/Chapters/Bandit.lean b/verso_blueprint/LMLBlueprint/Chapters/Bandit.lean deleted file mode 100644 index c3a5c74b..00000000 --- a/verso_blueprint/LMLBlueprint/Chapters/Bandit.lean +++ /dev/null @@ -1,543 +0,0 @@ -import Verso -import VersoManual -import VersoBlueprint -import LeanMachineLearning.SequentialLearning.Deterministic -import LeanMachineLearning.SequentialLearning.FiniteActions -import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace -import LeanMachineLearning.SequentialLearning.StationaryEnv -import LeanMachineLearning.Online.Bandit.ArrayProbSpace -import LeanMachineLearning.Online.Bandit.Regret -import LeanMachineLearning.Online.Bandit.RewardByCountMeasure -import LMLBlueprint.References -import LMLBlueprint.TeXPrelude - -open Verso.Genre -open Verso.Genre.Manual -open Informal - -#doc (Manual) "Stochastic multi-armed bandits" => - -A bandit algorithm is an algorithm in the sense of Definition TODO FIND OUT HOW TO REFERENCE OUTSIDE OF ENVIRONMENTS. -We call the actions _arms_ and the observations _rewards_. - -The first arm pulled by the algorithm is sampled from $`P_0`, the arm pulled at time $`1` is sampled from $`\pi_0(H_0)`, in which $`H_0 \in \mathcal{A} \times \mathcal{R}` is the data of the first arm pulled and the first observation received, and so on. - -A stochastic bandit is simply a reward distribution for each arm: a Markov kernel $`\nu : \mathcal{A} \rightsquigarrow \mathbb{R}`, conditional distribution of the rewards given the arm pulled. -It is a stationary environment in which the observation space is $`\mathcal{R} = \mathbb{R}`. - -An algorithm can interact with a bandit to produce a sequence of arms and rewards: after a time $`t`, the history $`H_t \in (\mathcal{A} \times \mathcal{R})^{t+1}` contains the arms pulled and rewards received up to that time, -- the algorithm chooses an arm $`A_{t+1}` sampled according to its policy $`\pi_t(H_t)`, -- the bandit generates a reward $`R_{t+1}` according to the distribution $`\nu(A_{t+1})`, -- the history is updated to $`H_{t+1} = ((A_0, R_0), \ldots, (A_{t+1}, R_{t+1}))`. - - - -# The array model of rewards - -:::group "bandit_space" -Probability space for stochastic multi-armed bandits -::: - -We previously built a probability space on which we can define the sequence of arms and rewards generated by the interaction between the algorithm and the bandit, using the Ionescu-Tulcea theorem. -From Theorem isAlgEnvSeq\_unique (TODO REF), we know that the law of the sequence of arms and rewards is independent of the probability space used to define them. -Nonetheless, we now build an alternative model of the rewards, on which it will be easier to prove concentration inequalities. -By the uniqueness of the law, these statements will then transfer to any algorithm-environment interaction. - -In the _array model_, we consider a probability space on which we have an infinite array of rewards from each arm, independent from each other. -When pulling an arm, the algorithm sees the next previously unseen reward from that arm in the array. - -:::definition "arrayMeasure" (parent := "bandit_space") (lean := "Bandits.ArrayModel.arrayMeasure, Bandits.ArrayModel.probSpace") -Let $`I = [0,1]` and let $`P_U` be the uniform distribution on $`I`. We define the probability space $`(\Omega_{\mathcal{A}}, P_{\mathcal{A}})`, where -- $` \Omega_{\mathcal{A}} := I^{\mathbb{N}} \times \mathcal{R}^{\mathbb{N} \times \mathcal{A}}` , -- $`P_{\mathcal{A}} := \left( \bigotimes_{n \in \mathbb{N}} P_U \right) \otimes \left( \bigotimes_{n \in \mathbb{N}, a \in \mathcal{A}} \nu(a) \right)` . - -Uses: {uses "ionescu-tulcea"}[]. -::: - - -:::definition "algFunction" (parent := "bandit_space") (lean := "Bandits.ArrayModel.algFunction, Bandits.ArrayModel.initAlgFunction") -Let $`\mathfrak{A}` be an {uses "algorithm"}[algorithm] with action space $`\mathcal{A}` and reward space $`\mathcal{R}`, policy $`\pi` and initial distribution $`P_0`. -For $`\mathcal{A}` and $`\mathcal{R}` standard Borel spaces, there exists jointly measurable functions $`f'_0 : I \to \mathcal{A}` and $`f_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times I \to \mathcal{A}` such that -- the law of $`f'_0` is $`P_0`, -- for all history $`h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}`, the law of $`f_t(h_t, \cdot)` is $`\pi_t(h_t)`. -::: - - -:::definition "AM.history" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hist, Bandits.ArrayModel.action, Bandits.ArrayModel.reward") -The history, actions and rewards on the {uses "arrayMeasure"}[array model probability space] $`(\Omega_{\mathcal{A}}, P_{\mathcal{A}})` are defined as follows: -- the action at time $`0` is $`A_0(\omega) = f'_0(\omega_{1,0})`, the reward at time $`0` is $`R_0(\omega) = \omega_{2,0,A_0(\omega)}`, and the history at time $`0` is $`H_0(\omega) = (A_0(\omega), R_0(\omega))`, -- for $`t \ge 0`, the action at time $`t+1` is $`A_{t+1}(\omega) = f_t(H_t(\omega), \omega_{1,t+1})`, the reward at time $`t+1` is $`R_{t+1}(\omega) = \omega_{2,N_{t+1,A_{t+1}(\omega)},A_{t+1}(\omega)}`, and the history at time $`t+1` is $`H_{t+1}(\omega) = (H_t(\omega), (A_{t+1}(\omega), R_{t+1}(\omega)))`. - -Uses: {uses "algFunction"}[], {uses "pullCount"}[]. -::: - - -The goal of this section is to show that $`(\Omega_{\mathcal{A}}, P_{\mathcal{A}})` with the actions and rewards defined above is an algorithm-environment sequence. - - - -## Measurability - -TODO: some of those results are proved for $`\mathcal{A}` countable. Add that assumption where needed. - -*Remark: Proving measurability with respect to a sub-sigma-algebra* - -In this section, we often need to prove that a random variable $`X` is measurable with respect to the sigma-algebra generated by a subset of the independent random variables defining the probability space $`\Omega_{\mathcal{A}}`. -We want to prove that $`X : \Omega_{\mathcal{A}} \to \mathcal{X}` is measurable with respect to the sigma-algebra $`\sigma((\omega_p)_{p \in S})`, where $`S` is a subset of the indices of the independent random variables defining $`\Omega_{\mathcal{A}}`. -In most cases, this is due to $`X` being defined (possibly recursively in a complicated way) only using those random variables. -However, it might be difficult to exhibit an explicit function $`f` such that $`X = f((\omega_p)_{p \in S})`. - -Here is a general strategy to prove such measurability results in Lean: -1. Prove that $`X` is measurable with respect to the full sigma-algebra on $`\Omega_{\mathcal{A}}`. -2. Prove a congruence lemma: for any $`\omega, \omega' \in \Omega_{\mathcal{A}}`, if $`\omega_p = \omega'_p` for all $`p \in S`, then $`X(\omega) = X(\omega')`. -3. Define $`g : (\prod_{p \in S} \Omega_p) \to \Omega` by $`g((\omega_p)_{p \in S}) = \omega'`, where $`\omega'_p = \omega_p` for $`p \in S` and $`\omega'_p` is some fixed value for $`p \notin S`. -4. Write $`X = X \circ g \circ \mathrm{proj}_S`, where $`\mathrm{proj}_S : \Omega_{\mathcal{A}} \to \prod_{p \in S} \Omega_p` is the projection on the coordinates in $`S`. -5. Conclude that $`X` is the composition of a measurable function $`(X \circ g)` and the random variable generating the sub-sigma-algebra, and thus is measurable with respect to that sub-sigma-algebra. - - -:::lemma_ "AM.measurable_hist" (parent := "bandit_space") (lean := "Bandits.ArrayModel.measurable_hist, Bandits.ArrayModel.measurable_action, Bandits.ArrayModel.measurable_reward") -$`H_t`, $`N_{t,A_t}`, $`A_t` and $`R_t` are measurable for all $`t \in \mathbb{N}`. - -Uses: {uses "AM.history"}[], {uses "algorithm"}[]. -::: - -:::proof "AM.measurable_hist" -Uses: {uses "AM.history"}[]. -::: - - -:::lemma_ "AM.hist_congr" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hist_congr") -Let $`\omega, \omega' \in \Omega_{\mathcal{A}}` and $`t \in \mathbb{N}`. -Suppose that -- $`\forall s \le t, \ \omega_{1,s} = \omega'_{1,s}` , -- $`\forall a \in \mathcal{A}, \forall s < N_{t+1,a}, \ \omega_{2,s,a} = \omega'_{2,s,a}` . - -Then $`H_t(\omega) = H_t(\omega')`. - -Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[]. -::: - -:::proof "AM.hist_congr" -Uses: {uses "AM.history"}[], {uses "pullCount_basic"}[]. -::: - - -:::lemma_ "AM.stepsUntil_congr" (parent := "bandit_space") (lean := "Bandits.ArrayModel.stepsUntil_congr") -Let $`\omega, \omega' \in \Omega_{\mathcal{A}}`, $`t, m \in \mathbb{N}` and $`a \in \mathcal{A}`. -Suppose that -- $` \omega_{1} = \omega'_{1}` , -- $`\forall s < m, \ \omega_{2,s,a} = \omega'_{2,s,a}` , -- $`\forall b \ne a, \forall s \in \mathbb{N}, \ \omega_{2,s,b} = \omega'_{2,s,b}` . - -Then $`(N_{t+1, a}(\omega) = m \wedge A_{t+1}(\omega) = a) \iff (N_{t+1, a}(\omega') = m \wedge A_{t+1}(\omega') = a)`. - -Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[]. -::: - -:::proof "AM.stepsUntil_congr" -Uses: {uses "AM.history"}[], {uses "AM.hist_congr"}[]. -::: - - -:::definition "AM.probSpaceSubsets" (parent := "bandit_space") (lean := "Bandits.ArrayModel.truePast") -We define the following functions on $`\Omega_{\mathcal{A}}`: -- $`F_{1, t}(\omega) = ((\omega_{1,s})_{s \le t}, (\omega_{2,s})_{s \in \mathbb{N}})` , -- $`F_{2, a, t}(\omega) = ((\omega_{1,s})_{s \in \mathbb{N}}, (\omega_{2, \min\{s,N_{t+1,a}(\omega)-1\}, a})_{s \in \mathbb{N}}, (\omega_{2, s, b})_{s \in \mathbb{N}, b \ne a})` , -- $`F_{2, a}^m(\omega) = ((\omega_{1,s})_{s \in \mathbb{N}}, (\omega_{2, \min\{s,m-1\}, a})_{s \in \mathbb{N}}, (\omega_{2, s, b})_{s \in \mathbb{N}, b \ne a})` . - -In the definition of $`F_{2, a, t}` and $`F_{2, a}^m`, if $`N_{t+1,a}(\omega) = 0` (resp. $`m = 0`), then the second component is a constant sequence equal to an arbitrary value. - -$`F_{1, t}(\omega)` contains all the information in $`\omega` except for the action selection randomness after time $`t`. - -$`F_{2, a, t}(\omega)` contains all the information in $`\omega` except the rewards for arm $`a` indexed by $`N_{t+1,a}(\omega)` or more. -$`F_{2, a}^m(\omega)` is similar, but removes the rewards for arm $`a` indexed by $`m` or more. - -Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[]. -::: - - -:::lemma_ "AM.measurable_hist_todo" (parent := "bandit_space") (lean := "Bandits.ArrayModel.measurable_hist_todo, Bandits.ArrayModel.measurable_hist_truePast") -For all $`t \in \mathbb{N}`, $`H_t` is measurable with respect to the sigma-algebra generated by $`F_{1, t}`, and with respect to the sigma-algebra generated by $`F_{2, a, t}` for any arm $`a \in \mathcal{A}`. - -Uses : {uses "algorithm"}[], {uses "AM.probSpaceSubsets"}[]. -::: - -:::proof "AM.measurable_hist_todo" -Uses: {uses "AM.measurable_hist"}[], {uses "pullCount"}[], {uses "AM.hist_congr"}[]. -::: - - -:::lemma_ "AM.measurable_action_add_one_truePast" (parent := "bandit_space") (lean := "Bandits.ArrayModel.measurable_action_add_one_truePast") -$`A_{t+1}` is measurable with respect to the sigma-algebra generated by $`F_{2, a, t}` for any arm $`a \in \mathcal{A}`. - -Uses : {uses "algorithm"}[], {uses "AM.probSpaceSubsets"}[]. -::: - -:::proof "AM.measurable_action_add_one_truePast" - Uses: {uses "AM.measurable_hist_todo"}[], . -::: - - -:::lemma_ "AM.measurable_pullCount_add_one_truePast" (parent := "bandit_space") (lean := "Bandits.ArrayModel.measurable_pullCount_add_one_truePast") -$`N_{t+1,a}` is measurable with respect to the sigma-algebra generated by $`F_{2, a, t}`. - -Uses: {uses "AM.history"}[], {uses "arrayMeasure"}[], {uses "algorithm"}[], {uses "AM.probSpaceSubsets"}[], {uses "pullCount"}[]. -::: - -:::proof "AM.measurable_pullCount_add_one_truePast" - Uses: {uses "AM.measurable_hist_todo"}[]. -::: - - -:::lemma_ "AM.measurable_stepsUntil" (parent := "bandit_space") (lean := "Bandits.ArrayModel.measurable_stepsUntil") -For $`t, m \in \mathbb{N}` and $`a \in \mathcal{A}`, the indicator function $`\mathbb{I}\{N_{t+1,a} = m \wedge A_{t+1} = a\} : \Omega_{\mathcal{A}} \to \{0, 1\}` is measurable with respect to the sigma-algebra generated by $`F_{2, a}^m`. - -Uses: {uses "AM.history"}[], {uses "arrayMeasure"}[], {uses "algorithm"}[], {uses "pullCount"}[], {uses "AM.probSpaceSubsets"}[]. -::: - -:::proof "AM.measurable_stepsUntil" - Uses: {uses "AM.measurable_hist"}[], {uses "AM.stepsUntil_congr"}[]. -::: - - -:::lemma_ "AM.measurable_pullCount_action_add_one_hist" (parent := "bandit_space") (lean := "Bandits.ArrayModel.measurable_pullCount_action_add_one_hist") -For $`t \in \mathbb{N}`, the function $`N_{t+1, A_{t+1}}` is measurable with respect to the sigma-algebra generated by $`H_t` and $`A_{t+1}`. - -Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[]. -::: - -:::proof "AM.measurable_pullCount_action_add_one_hist" -::: - - - -## Independence - - -:::lemma_ "AM.indepFun_fst_add_one_aux" (parent := "bandit_space") (lean := "Bandits.ArrayModel.indepFun_fst_add_one_aux") -$`\omega \mapsto \omega_{1, t+1}` is independent of $`F_{1, t}`. - -Uses: {uses "AM.probSpaceSubsets"}[]. -::: - - -:::lemma_ "AM.indepFun_fst_add_one_hist" (parent := "bandit_space") (lean := "Bandits.ArrayModel.indepFun_fst_add_one_hist") -$`\omega \mapsto \omega_{1, t+1}` is independent of $`H_t`. - -Uses: {uses "algorithm"}[], {uses "AM.probSpaceSubsets"}[]. -::: - -:::proof "AM.indepFun_fst_add_one_hist" - Uses: {uses "AM.measurable_hist_todo"}[], {uses "AM.indepFun_fst_add_one_aux"}[] -::: - - -:::lemma_ "AM.indepFun_snd_apply_aux" (parent := "bandit_space") (lean := "Bandits.ArrayModel.indepFun_snd_apply_aux") -For $`a \in \mathcal{A}` and $`m \in \mathbb{N}`, $`\omega \mapsto \omega_{2, m, a}` is independent of $`F_{2, a}^m`. - -Uses: {uses "AM.probSpaceSubsets"}[]. -::: - - - -:::lemma_ "AM.indepFun_snd_apply_pullCount_action" (parent := "bandit_space") (lean := "Bandits.ArrayModel.indepFun_snd_apply_pullCount_action") -For $`a \in \mathcal{A}` and $`m \in \mathbb{N}`, $`\omega \mapsto \omega_{2, m, a}` is independent of the indicator function $`\mathbb{I}\{N_{t+1,a} = m \wedge A_{t+1} = a\}`. - -Uses: {uses "algorithm"}[], {uses "pullCount"}[], {uses "AM.probSpaceSubsets"}[]. -::: - -:::proof "AM.indepFun_snd_apply_pullCount_action" - Uses: {uses "AM.indepFun_snd_apply_aux"}[], {uses "AM.measurable_stepsUntil"}[] -::: - - -:::lemma_ "AM.indepFun_snd_hist_cond" (parent := "bandit_space") (lean := "Bandits.ArrayModel.indepFun_snd_hist_cond") -For $`a \in \mathcal{A}` and $`t, m \in \mathbb{N}`, $`\omega \mapsto \omega_{2, m, a}` is independent of $`H_t` given that $`N_{t+1,a} = m` and $`A_{t+1} = a`. - -Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[]. -::: - -:::proof "AM.indepFun_snd_hist_cond" - Uses: {uses "AM.measurable_hist_todo"}[], {uses "AM.measurable_hist"}[], {uses "AM.indepFun_snd_apply_aux"}[], {uses "AM.measurable_stepsUntil"}[], {uses "AM.probSpaceSubsets"}[]. -::: - - - - -## Laws - - -:::lemma_ "AM.hasLaw_action_zero" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hasLaw_action_zero") -The law of $`A_0` in the array model is $`P_0`. - -Uses : {uses "AM.history"}[], {uses "algorithm"}[]. -::: - -:::proof "AM.hasLaw_action_zero" - Uses: {uses "AM.measurable_hist"}[] -::: - - -:::lemma_ "AM.hasCondDistrib_reward_zero" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hasCondDistrib_reward_zero") -In the array model, $`P_{\mathcal{A}}(R_0 \mid A_0) = \nu`. - -Uses: {uses "AM.history"}[], {uses "algorithm"}[]. -::: - -:::proof "AM.hasCondDistrib_reward_zero" - Uses: {uses "AM.measurable_hist"}[], {uses "condDistrib_ae_eq_cond"}[] -::: - - -:::lemma_ "AM.hasCondDistrib_action" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hasCondDistrib_action") -In the array model, $`P_{\mathcal{A}}(A_{t+1} \mid H_t) = \pi_t`. - -Uses: {uses "AM.history"}[], {uses "algorithm"}[]. -::: - -:::proof "AM.hasCondDistrib_action" - Uses: {uses "AM.measurable_hist"}[], {uses "AM.indepFun_fst_add_one_hist"}[] -::: - - -:::lemma_ "AM.hasCondDistrib_reward_pullCount_action" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hasCondDistrib_reward_pullCount_action") -In the array model, $`P_{\mathcal{A}}(R_{t+1} \mid N_{t+1,A_{t+1}}, A_{t+1}) = \nu`. - -Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[]. -::: - -:::proof "AM.hasCondDistrib_reward_pullCount_action" - Uses: {uses "AM.indepFun_snd_apply_pullCount_action"}[], {uses "AM.measurable_hist"}[], {uses "pullCount_basic"}[], {uses "condDistrib_ae_eq_cond"}[] -::: - - -:::lemma_ "AM.hasCondDistrib_reward_hist_action_pullCount" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hasCondDistrib_reward_hist_action_pullCount") -In the array model, $`P_{\mathcal{A}}(R_{t+1} \mid H_t, A_{t+1}, N_{t+1,A_{t+1}}) = \nu`. - -Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[]. -::: - -:::proof "AM.hasCondDistrib_reward_hist_action_pullCount" - Uses: {uses "AM.indepFun_snd_apply_pullCount_action"}[], {uses "AM.indepFun_snd_hist_cond"}[], {uses "AM.measurable_hist"}[], {uses "pullCount_basic"}[] -::: - - -:::lemma_ "AM.condIndepFun_reward_hist" (parent := "bandit_space") (lean := "Bandits.ArrayModel.condIndepFun_reward_hist") -For $`t \ge 0`, $`R_{t+1} \ind H_t \mid A_{t+1}, N_{t+1, A_{t+1}}`. - -Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[], {uses "AM.measurable_hist"}[]. -::: - -:::proof "AM.condIndepFun_reward_hist" - Uses: {uses "AM.measurable_hist"}[], {uses "AM.hasCondDistrib_reward_hist_action_pullCount"}[] -::: - - -:::lemma_ "AM.hasCondDistrib_reward" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hasCondDistrib_reward") -In the array model, $`P_{\mathcal{A}}(R_{t+1} \mid H_t, A_{t+1}) = \nu`. - -Uses: {uses "AM.history"}[], {uses "stationaryEnv"}[], {uses "environment"}[], {uses "algorithm"}[]. -::: - -:::proof "AM.hasCondDistrib_reward" - Uses: {uses "AM.measurable_pullCount_action_add_one_hist"}[], {uses "AM.hasCondDistrib_reward_pullCount_action"}[], {uses "AM.measurable_hist"}[], {uses "AM.condIndepFun_reward_hist"}[], {uses "pullCount"}[] -::: - - -:::theorem "isAlgEnvSeq_arrayMeasure" (parent := "bandit_space") (lean := "Bandits.ArrayModel.isAlgEnvSeq_arrayMeasure") -The actions and rewards defined on the array model probability space $`(\Omega_{\mathcal{A}}, P_{\mathcal{A}})` form an algorithm-environment sequence for the algorithm $`\mathfrak{A}` and bandit $`\nu`. - -Uses: {uses "AM.history"}[], {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[]. -::: - -:::proof "isAlgEnvSeq_arrayMeasure" -The four conditions of {uses "IsAlgEnvSeq"}[] are satisfied by {uses "AM.hasLaw_action_zero"}[], {uses "AM.hasCondDistrib_reward_zero"}[], {uses "AM.hasCondDistrib_action"}[] and {uses "AM.hasCondDistrib_reward"}[]. -::: - - - -# Law of the n-th pull - -:::group "rewardByCount_law" -Law of the n-th pull -::: - -This section describes the law of $`Y_{n, a}` the $`n^{th}` reward obtained from an arm $`a \in \mathcal{A}`. - -We augment the probability space $`\Omega` on which we have an algorithm-environment sequence with $`\Omega' = \mathbb{R}^{\mathbb{N} \times \mathcal{A}}`, on which we put the product measure $`\bigotimes_{n \in \mathbb{N}, a \in \mathcal{A}} \nu(a)`. -With that measure, the law of $`Z_{n,a}` is $`\nu(a)`. - - -:::lemma_ "measurable_comap_indicator_stepsUntil_eq" (parent := "rewardByCount_law") (lean := "Learning.measurable_comap_indicator_stepsUntil_eq") -The function $`\mathbb{I}\{T_{n,a} = t\} : \Omega \to \{0, 1\}` is measurable with respect to the sigma-algebra generated by $`(H_{t-1}, A_t)`. - -Uses: {uses "history"}[], {uses "stepsUntil"}[]. -::: - -:::proof "measurable_comap_indicator_stepsUntil_eq" - Uses: {uses "stepsUntil_basic"}[], {uses "pullCount_basic"}[], {uses "pullCount"}[], {uses "IsAlgEnvSeq.filtration"}[]. -::: - - -:::lemma_ "CondIndepFun.prod_right" (lean := "ProbabilityTheory.CondIndepFun.prod_right") -If $`X \ind Y \mid Z`, then $`X \ind (Y, Z) \mid Z`. -::: - - -:::lemma_ "condIndepFun_reward_stepsUntil_arm" (parent := "rewardByCount_law") (lean := "Bandits.condIndepFun_reward_stepsUntil_action") -For $`t > 0`, $`R_t \ind \mathbb{I}\{T_{n, a} = t\} \mid A_t`. - -Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "ionescu-tulcea"}[], {uses "stepsUntil"}[]. -::: - -:::proof "condIndepFun_reward_stepsUntil_arm" -$`\mathbb{I}\{T_{n, a} = t\}` is measurable with respect to the sigma-algebra generated by $`(H_{t-1}, A_t)` by {uses "measurable_comap_indicator_stepsUntil_eq"}[]. - -It thus suffices to show that $`R_t \ind (H_{t-1}, A_t) \mid A_t`, which is implied by $`R_t \ind H_{t-1} \mid A_t` ({uses "CondIndepFun.prod_right"}[]), which is {uses "condIndepFun_reward_hist_action"}[]. - -Uses: {uses "condIndepFun_reward_hist_action"}[], {uses "CondIndepFun.prod_right"}[], {uses "stepsUntil_basic"}[], {uses "measurable_comap_indicator_stepsUntil_eq"}[], {uses "history"}[], {uses "pullCount"}[]. -::: - - -:::lemma_ "reward_cond_stepsUntil" (parent := "rewardByCount_law") (lean := "Bandits.reward_cond_stepsUntil") -Let $`n > 0`, $`t \in \mathbb{N}` and suppose that $`P(T_{n, a} = t) > 0`. -Then $`P(R_t \mid T_{n, a} = t) = \nu(a)`. - -Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "ionescu-tulcea"}[], {uses "stepsUntil"}[]. -::: - -:::proof "reward_cond_stepsUntil" -First, if $`T_{n, a} = t`, then $`A_t = a` ({uses "stepsUntil_basic"}[]), such that $`P(R_t \mid T_{n, a} = t) = P(R_t \mid T_{n, a} = t, A_t = a)`. - -Then, using first the independence from {uses "condIndepFun_reward_stepsUntil_arm"}[] and then the conditional distribution from {uses "condDistrib_reward_stationaryEnv"}[], we have -$$` - P(R_t \mid T_{n, a} = t, A_t = a) - = P(R_t \mid A_t = a) - = \nu(a) - \: . -` - -Uses: {uses "environment"}[], {uses "stepsUntil_basic"}[], {uses "condIndepFun_reward_stepsUntil_arm"}[], {uses "pullCount"}[], {uses "condDistrib_ae_eq_cond"}[], {uses "condDistrib_reward_stationaryEnv"}[] -::: - - -:::lemma_ "condDistrib_ae_eq_cond" (lean := "ProbabilityTheory.condDistrib_ae_eq_cond") -For a random variable $`X` on a countable space with the discrete sigma algebra, $`P(Y \mid X) = (x \mapsto P(Y \mid X = x))`, $`(X_*P)`-almost surely. -Furthermore, that almost sure equality means that for all $`x` such that $`P(X = x) > 0`, we have $`P(Y \mid X = x) = P(Y \mid X)(x)`. -::: - - -:::lemma_ "condDistrib_rewardByCount_stepsUntil" (parent := "rewardByCount_law") (lean := "Bandits.condDistrib_rewardByCount_stepsUntil") -For $`n > 0` and $`t \in \mathbb{N}`, $`P(Y_{n,a} \mid T_{n,a}) = \nu(a)` (in which the measure on the r.h.s. is seen as a constant kernel). - -Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "ionescu-tulcea"}[], {uses "rewardByCount"}[], {uses "stepsUntil"}[]. -::: - -:::proof "condDistrib_rewardByCount_stepsUntil" -It suffices to show that for all $`t \in \mathbb{N} \cup \{\infty\}` such that $`P(T_{n, a} = t) > 0`, the law of $`Y_{n,a}` conditioned on $`T_{n,a} = t` is $`\nu(a)`. - -If $`t < \infty`, then $`P(Y_{n, a} \mid T_{n, a = t}) = P(R_t \mid T_{n, a} = t) = \nu(a)` by {uses "reward_cond_stepsUntil"}[]. - -If $`t = \infty`, then $`P(Y_{n, a} \mid T_{n, a} = \infty) = P(Z_{n, a} \mid T_{n, a} = \infty)`. By independence of $`Z_{n,a}` and $`T_{n, a}`, this is just $`\nu(a)`, the law of $`Z_{n,a}`. - -Uses: {uses "environment"}[], {uses "reward_cond_stepsUntil"}[], {uses "pullCount"}[], {uses "condDistrib_ae_eq_cond"}[] -::: - - -:::lemma_ "hasLaw_rewardByCount" (parent := "rewardByCount_law") (lean := "Bandits.hasLaw_rewardByCount") -For $`n > 0` and $`a \in \mathcal{A}`, $`(Y_{n,a})_*P = \nu(a)`. - -Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "ionescu-tulcea"}[], {uses "rewardByCount"}[] -::: - -:::proof "hasLaw_rewardByCount" -The law of $`Y_{n,a}` is given by $`(Y_{n, a})_*P = P(Y_{n, a} \mid T_{n, a}) \circ (T_{n, a})_*P`. -By {uses "condDistrib_rewardByCount_stepsUntil"}[], $`P(Y_{n, a} \mid T_{n, a}) = \nu(a)`, a constant kernel. -Thus the composition is just $`\nu(a)`. - -Uses: {uses "environment"}[], {uses "condDistrib_rewardByCount_stepsUntil"}[], {uses "stepsUntil"}[], {uses "pullCount"}[]. -::: - - - -# Regret and other bandit quantities - -:::group "regret" -Regret and other bandit quantities -::: - -For an arm $`a \in \mathcal{A}`, we denote by $`\mu_a` the mean of the rewards for that arm, that is $`\mu_a = \nu(a)[\mathrm{id}]`. -We denote by $`\mu^*` the mean of the best arm, that is $`\mu^* = \max_{a \in \mathcal{A}} \mu_a`. - - -:::definition "regret" (parent := "regret") (lean := "Bandits.regret") -The regret $`R_T` of a sequence of arms $`A_0, \ldots, A_{T-1}` after $`T` pulls is the difference between the cumulative reward of always playing the best arm and the cumulative reward of the sequence: -$$` - R_T = T \mu^* - \sum_{t=0}^{T-1} \mu_{A_t} \: . -` -::: - -TODO: the $`R_T` notation clashes with the random variable $`R_t`. - -:::definition "gap" (parent := "regret") (lean := "Bandits.gap") -For an arm $`a \in \mathcal{A}`, its gap is defined as the difference between the mean of the best arm and the mean of that arm: $`\Delta_a = \mu^* - \mu_a`. -::: - - -:::lemma_ "sum_pullCount_mul" (parent := "regret") (lean := "Learning.sum_pullCount_mul") -Let $`f : \mathcal{A} \to \mathbb{R}` be a function on the arms. For all $`t \in \mathbb{N}`, -$$` - \sum_{a \in \mathcal{A}} N_{t,a} f(a) = \sum_{s=0}^{t-1} f(A_s) \: . -` - -Uses: {uses "pullCount"}[]. -::: - -:::proof "sum_pullCount_mul" -$$` - \sum_{a \in \mathcal{A}} N_{t,a} f(a) - &= \sum_{a \in \mathcal{A}} \sum_{s=0}^{t-1} \mathbb{I}\{A_s = a\} f(a) - \\ - &= \sum_{s=0}^{t-1} \sum_{a \in \mathcal{A}} \mathbb{I}\{A_s = a\} f(a) - \\ - &= \sum_{s=0}^{t-1} f(A_s) - \: . -` -::: - - -:::lemma_ "regret_eq_sum_pullCount_mul_gap" (parent := "regret") (lean := "Bandits.regret_eq_sum_pullCount_mul_gap") -For $`\mathcal{A}` finite, the {uses "regret"}[regret] $`R_T` can be expressed as a sum over the arms and their {uses "gap"}[gaps]: -$$` - R_T = \sum_{a \in \mathcal{A}} N_{T,a} \Delta_a \: . -` - -Uses: {uses "pullCount"}[]. -::: - -:::proof "regret_eq_sum_pullCount_mul_gap" -Apply {uses "sum_pullCount_mul"}[] with $`f(a) = \Delta_a` to obtain: -$$` - \sum_{a \in \mathcal{A}} N_{T,a} \Delta_a - &= \sum_{s=0}^{T-1} \Delta_{A_s} - \\ - &= \sum_{s=0}^{T-1} \mu^* - \sum_{s=0}^{T-1} \mu_{A_s} - \\ - &= R_T - \: . -` -::: - - -:::lemma_ "integral_regret_eq_sum_mul" (parent := "regret") (lean := "Bandits.integral_regret_eq_sum_gap_mul_integral_pullCount") -For $`\mathcal{A}` finite, the expected {uses "regret"}[regret] can be expressed as a sum over the arms and their {uses "gap"}[gaps]: -$$` - P[R_T] = \sum_{a \in \mathcal{A}}P[N_{T,a}] \Delta_a \: . -` - -Uses: {uses "pullCount"}[]. -::: - -:::proof "integral_regret_eq_sum_mul" -Uses: {uses "regret_eq_sum_pullCount_mul_gap"}[]. -::: diff --git a/verso_blueprint/LMLBlueprint/Chapters/BanditAlgs.lean b/verso_blueprint/LMLBlueprint/Chapters/BanditAlgs.lean deleted file mode 100644 index 61b21a58..00000000 --- a/verso_blueprint/LMLBlueprint/Chapters/BanditAlgs.lean +++ /dev/null @@ -1,332 +0,0 @@ -import Verso -import VersoManual -import VersoBlueprint -import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin -import LeanMachineLearning.SequentialLearning.Deterministic -import LeanMachineLearning.SequentialLearning.FiniteActions -import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace -import LeanMachineLearning.SequentialLearning.StationaryEnv -import LeanMachineLearning.Online.Bandit.Algorithms.ETC -import LeanMachineLearning.Online.Bandit.Algorithms.UCB -import LeanMachineLearning.Online.Bandit.ArrayProbSpace -import LeanMachineLearning.Online.Bandit.Regret -import LeanMachineLearning.Online.Bandit.RewardByCountMeasure -import LeanMachineLearning.Online.Bandit.SumRewards -import LeanMachineLearning.Probability.Moments.SubGaussian -import LMLBlueprint.References -import LMLBlueprint.TeXPrelude -import Mathlib.Probability.Moments.SubGaussian - -open Verso.Genre -open Verso.Genre.Manual -open Informal - -#doc (Manual) "Bandit algorithms" => - -:::group "banditAlgorithms" -Bandit algorithms -::: - - -# Round-Robin - -This is not an interesting bandit algorithm per se, but it is used as a subroutine in other algorithms and can be a simple baseline. -This algorithm simply cycles through the arms in order. - -:::definition "roundRobinAlgorithm" (parent := "banditAlgorithms") (lean := "Learning.RoundRobin.nextAction, Learning.roundRobinAlgorithm") -The Round-Robin algorithm is the {uses "detAlgorithm"}[deterministic algorithm] defined as follows: at time $`t \in \mathbb{N}`, $`A_t = t \mod K`. -::: - - -:::lemma_ "pullCount_roundRobinAlgorithm" (parent := "banditAlgorithms") (lean := "Learning.RoundRobin.pullCount_mul") -For the Round-Robin algorithm, for any arm $`a \in [K]`, at time $`Km` we have -$$` - N_{Km,a} = m \: . -` - -Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[] , {uses "pullCount"}[], {uses "roundRobinAlgorithm"}[]. -::: - -:::proof "pullCount_roundRobinAlgorithm" - Uses {uses "environment"}[], {uses "history"}[], {uses "pullCount_basic"}[], {uses "roundRobinAlgorithm"}[] -::: - - -TODO: regret. - - - - -# Explore-Then-Commit - -Note: times start at 0 to be consistent with Lean. - -Note: we will describe the algorithm by writing $`A_t = ...`, but our formal bandit model needs a policy $`\pi_t` that gives the distribution of the arm to pull. What me mean is that $`\pi_t` is a Dirac distribution at that arm. - -:::definition "etcAlgorithm" (parent := "banditAlgorithms") (lean := "Bandits.ETC.nextArm, Bandits.etcAlgorithm") -The Explore-Then-Commit (ETC) algorithm with parameter $`m \in \mathbb{N}` is the {uses "detAlgorithm"}[deterministic algorithm] defined as follows: -1. for $`t < Km`, $`A_t = t \mod K` (pull each arm $`m` times), -2. compute $`\hat{A}_m^* = \arg\max_{a \in [K]} \hat{\mu}_a`, where $`\hat{\mu}_a = \frac{1}{m} \sum_{t=0}^{Km-1} \mathbb{I}(A_t = a) X_t` is the empirical mean of the rewards for arm $`a`, -3. for $`t \ge Km`, $`A_t = \hat{A}_m^*` (pull the empirical best arm). -::: - -:::lemma_ "ETC.isAlgEnvSeqUntil_roundRobinAlgorithm" (parent := "banditAlgorithms") (lean := "Bandits.ETC.isAlgEnvSeqUntil_roundRobinAlgorithm") - -An {uses "IsAlgEnvSeq"}[algorithm-environment sequence] for the {uses "etcAlgorithm"}[Explore-Then-Commit algorithm] with parameter $`m` is an algorithm-environment sequence for the {uses "roundRobinAlgorithm"}[Round-Robin algorithm] until time $`Km - 1`. -That is, ETC plays the same as Round-Robin until time $`Km - 1`. - -Uses {uses "stationaryEnv"}[]. -::: - - -:::lemma_ "pullCount_etcAlgorithm" (parent := "banditAlgorithms") (lean := "Bandits.ETC.pullCount_of_ge") -For the {uses "etcAlgorithm"}[Explore-Then-Commit algorithm] with parameter $`m`, for any arm $`a \in [K]` and any time $`t \ge Km`, we have -$$` - N_{t,a} - = m + (t - Km) \mathbb{I}\{\hat{A}_m^* = a\} - \: . -` - -Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "pullCount"}[]. -::: - -:::proof "pullCount_etcAlgorithm" - Uses: {uses "pullCount_roundRobinAlgorithm"}[], {uses "ETC.isAlgEnvSeqUntil_roundRobinAlgorithm"}[] -::: - -:::lemma_ "sumRewards_bestArm_le_of_arm_mul_eq" (parent := "banditAlgorithms") (lean := "Bandits.ETC.sumRewards_bestArm_le_of_arm_mul_eq") -If $`\hat{A}_m^* = a`, then we have $`S_{Km, a^*} \le S_{Km, a}`. - -Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "sumRewards"}[], {uses "etcAlgorithm"}[] -::: - -:::proof "sumRewards_bestArm_le_of_arm_mul_eq" - Uses: {uses "environment"}[], {uses "history"}[], {uses "pullCount"}[], {uses "empMean"}[], {uses "etcAlgorithm"}[] -::: - - -:::lemma_ "prob_etc_error_le_exp" (parent := "banditAlgorithms") (lean := "Bandits.ETC.prob_arm_mul_eq_le") -Suppose that $`\nu(a)` is $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] for all arms $`a \in [K]`. -Then for the {uses "etcAlgorithm"}[Explore-Then-Commit algorithm] with parameter $`m`, for any arm $`a \in [K]` with $`\Delta_a > 0`, we have $`P(\hat{A}_m^* = a) \le \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right)`. - -Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "gap"}[] -::: - -:::proof "prob_etc_error_le_exp" -By {uses "sumRewards_bestArm_le_of_arm_mul_eq"}[], -$$` - P(\hat{A}_m^* = a) - \le P(S_{Km, a} \ge S_{Km, a^*}) - \: . -` -By {uses "prob_sumRewards_le_sumRewards_le"}[], and then the concentration inequality of {uses "probReal_sum_le_sum_streamMeasure"}[] we have -$$` - P\left(S_{Km, a^*} \le S_{Km, a}\right) - &\le (\otimes_a \nu(a))^{\otimes \mathbb{N}} \left( \sum_{s=0}^{m-1} \omega_{s, a^*} \le \sum_{s=0}^{m-1} \omega_{s, a} \right) - \\ - &\le \exp\left( -m \frac{\Delta_a^2}{4 \sigma^2} \right) - \: . -` - -Uses: {uses "environment"}[], {uses "pullCount"}[], {uses "etcAlgorithm"}[] -::: - - -:::theorem "regret_etc_le" (parent := "banditAlgorithms") (lean := "Bandits.ETC.regret_le") -Suppose that $`\nu(a)` is $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] for all arms $`a \in [K]`. -Then for {uses "etcAlgorithm"}[Explore-Then-Commit algorithm] with parameter $`m`, the expected regret after $`T` pulls with $`T \ge Km` is bounded by -$$` - P[R_T] - \le m \sum_{a=1}^K \Delta_a + (T - Km) \sum_{a=1}^K \Delta_a \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right) - \: . -` - -Uses: {uses "stationaryEnv"}[], {uses "regret"}[], {uses "IsAlgEnvSeq"}[], {uses "gap"}[] -::: - -:::proof "regret_etc_le" -By {uses "regret_eq_sum_pullCount_mul_gap"}[], we have $`P[R_T] = \sum_{a=1}^K P\left[N_{T,a}\right] \Delta_a`~. -It thus suffices to bound $`P[N_{T,a}]` for each arm $`a` with $`\Delta_a > 0`. -It suffices to prove that -$$` - P[N_{T,a}] - \le m + (T - Km) \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right) - \: . -` - -By {uses "pullCount_etcAlgorithm"}[], -$$` - N_{T,a} - = m + (T - Km) \mathbb{I}\{\hat{A}_m^* = a\} - \: . -` - -It thus suffices to prove the inequality $`P(\hat{A}_m^* = a) \le \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right)` for $`\Delta_a > 0`. -This is done in {uses "prob_etc_error_le_exp"}[]. - - -Uses: {uses "integral_regret_eq_sum_mul"}[], {uses "pullCount_basic"}[], -::: - - -# UCB - -:::definition "ucbAlgorithm" (parent := "banditAlgorithms") (lean := "Bandits.UCB.nextArm, Bandits.ucbAlgorithm") -The UCB algorithm with parameter $`c \in \mathbb{R}_+` is the {uses "detAlgorithm"}[deterministic algorithm] defined as follows: -1. for $`t < K`, $`A_t = t \mod K` (pull each arm once), -2. for $`t \ge K`, $`A_t = \arg\max_{a \in [K]} \left( \hat{\mu}_{t,a} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,a}}} \right)`, where $`\hat{\mu}_{t,a} = \frac{1}{N_{t,a}} \sum_{s=0}^{t-1} \mathbb{I}(A_s = a) X_s` is the empirical mean of the rewards for arm `a`. -::: - - -Note: the argmax in the second step is chosen in a measurable way. - - -:::lemma_ "UCB.isAlgEnvSeqUntil_roundRobinAlgorithm" (parent := "banditAlgorithms") (lean := "Bandits.UCB.isAlgEnvSeqUntil_roundRobinAlgorithm") -An {uses "IsAlgEnvSeq"}[algorithm-environment sequence] for the {uses "ucbAlgorithm"}[UCB algorithm] is an algorithm-environment sequence for the {uses "roundRobinAlgorithm"}[Round-Robin algorithm] until time $`K - 1`. -That is, UCB plays the same as Round-Robin until time $`K - 1`. - -Uses: {uses "stationaryEnv"}[]. -::: - - -:::lemma_ "ucbIndex_le_ucbIndex_arm" (parent := "banditAlgorithms") (lean := "Bandits.UCB.ucbIndex_le_ucbIndex_arm") -For the {uses "ucbAlgorithm"}[UCB algorithm], for all time $`t \ge K` and arm $`a \in [K]`, we have -$$` - \hat{\mu}_{t,a} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,a}}} - \le \hat{\mu}_{t,A_t} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,A_t}}} - \: . -` - -Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "pullCount"}[], {uses "empMean"}[] -::: - -:::proof "ucbIndex_le_ucbIndex_arm" -By definition of the algorithm. -::: - - -:::lemma_ "gap_arm_le_two_mul_ucbWidth" (parent := "banditAlgorithms") (lean := "Bandits.UCB.gap_arm_le_two_mul_ucbWidth, Bandits.UCB.pullCount_arm_le") -Suppose that we have the 3 following conditions: -1. $`\mu^* \le \hat{\mu}_{t, a^*} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,a^*}}}`, -2. $`\hat{\mu}_{t,A_t} - \sqrt{\frac{2 c \log(t + 1)}{N_{t,A_t}}} \le \mu_{A_t}`, -3. $`\hat{\mu}_{t, a^*} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,a^*}}} \le \hat{\mu}_{t,A_t} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,A_t}}}`. - -Then if $`N_{t,A_t} > 0` we have -$$` - \Delta_{A_t} - \le 2 \sqrt{\frac{2 c \log(t + 1)}{N_{t,A_t}}} - \: . -` - -And in turn, if $`\Delta_{A_t} > 0` we get -$$` - N_{t,A_t} - \le \frac{8 c \log(t + 1)}{\Delta_{A_t}^2} - \: . -` - -Note that the third condition is always satisfied for UCB by {uses "ucbIndex_le_ucbIndex_arm"}[], but this lemma, as stated, is independent of the UCB algorithm. - -Uses: {uses "pullCount"}[], {uses "gap"}[], {uses "empMean"}[]. -::: - - -:::lemma_ "prob_ucbIndex_le" (parent := "banditAlgorithms") (lean := "Bandits.UCB.prob_ucbIndex_le") -Suppose that $`\nu(a)` is $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] for all arms $`a \in [K]`. -Let $`c \ge 0` be a real number. -Then for any time $`n \in \mathbb{N}` and any arm $`a \in [K]`, we have -$$` - P\left(0 < N_{n, a} \ \wedge \ \hat{\mu}_{n, a} + \sqrt{\frac{2 c \sigma^2 \log(n + 1)}{N_{n,a}}} \le \mu_a\right) - \le \frac{1}{(n + 1)^{c - 1}} - \: . -` - -And also, -$$` - P\left(0 < N_{n, a} \ \wedge \ \hat{\mu}_{n, a} - \sqrt{\frac{2 c \sigma^2 \log(n + 1)}{N_{n,a}}} \ge \mu_a\right) - \le \frac{1}{(n + 1)^{c - 1}} - \: . -` - -Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "pullCount"}[], {uses "empMean"}[] -::: - -:::proof "prob_ucbIndex_le" - Uses: {uses "prob_sum_le_sqrt_log"}[], {uses "ionescu-tulcea"}[], {uses "prob_pullCount_prod_sumRewards_mem_le"}[]. -::: - - -:::lemma_ "pullCount_le_add_three" (parent := "banditAlgorithms") -For $`C` a natural number, for any time $`n \in \mathbb{N}` and any arm $`a \in [K]`, we have -$$` - N_{n,a} - &\le C + 1 - \\&\quad + - \sum_{s=1}^{n-1} \mathbb{I}\{A_s = a \ \wedge \ C < N_{s,a} \ \wedge \ - \mu^* \le \hat{\mu}_{s, a^*} + \sqrt{\frac{2 c \sigma^2 \log(s + 1)}{N_{s,a^*}}} \ \wedge \ - \hat{\mu}_{s, A_s} - \sqrt{\frac{2 c \sigma^2 \log(s + 1)}{N_{s,A_s}}} \le \mu_{A_s}\} - \\&\quad + - \sum_{s=1}^{n-1} - \mathbb{I}\{0 < N_{s, a^*} \ \wedge \ \hat{\mu}_{s, a^*} + \sqrt{\frac{2 c \sigma^2 \log(s + 1)}{N_{s,a^*}}} < - \mu^*\} - \\&\quad + - \sum_{s=1}^{n-1} - \mathbb{I}\{0 < N_{s, a} \ \wedge \ \mu_a < - \hat{\mu}_{s, a} - \sqrt{\frac{2 c \sigma^2 \log(s + 1)}{N_{s,a}}}\} -` - -Uses: {uses "pullCount"}[], {uses "empMean"}[], {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "ucbAlgorithm"}[]. -::: - -:::proof "pullCount_le_add_three" - Uses: {uses "environment"}[], {uses "ucbAlgorithm"}[], {uses "pullCount_basic"}[] -::: - - -:::lemma_ "some_sum_eq_zero" (parent := "banditAlgorithms") -For the {uses "ucbAlgorithm"}[UCB algorithm] with parameter $`c \sigma^2 \ge 0`, for any time $`n \in \mathbb{N}` and any arm $`a \in [K]` with positive gap, the first sum in {uses "pullCount_le_add_three"}[] is equal to zero for positive $`C` such that $`C \ge \frac{8 c \sigma^2 \log(n + 1)}{\Delta_a^2}`. - -Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "ucbAlgorithm"}[], {uses "pullCount"}[], {uses "gap"}[], {uses "empMean"}[]. - -The Lean declaration is "Bandits.UCB.some\_sum\_eq\_zero" but adding it causes a strange error, so I removed it. -::: - -:::proof "some_sum_eq_zero" - Uses: {uses "environment"}[], {uses "ucbAlgorithm"}[], {uses "ucbIndex_le_ucbIndex_arm"}[], {uses "pullCount_basic"}[], {uses "gap_arm_le_two_mul_ucbWidth"}[] -::: - - -:::lemma_ "expectation_pullCount_le" (parent := "banditAlgorithms") (lean := "Bandits.UCB.expectation_pullCount_le") -Suppose that $`\nu(a)` is $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] for all arms $`a \in [K]`. -For the {uses "ucbAlgorithm"}[UCB algorithm] with parameter $`c \sigma^2 > 0`, for any time $`n \in \mathbb{N}` and any arm $`a \in [K]` with positive {uses "gap"}[gap], we have -$$` - P[N_{n,a}] - \le \frac{8 c \sigma^2 \log(n + 1)}{\Delta_a^2} + 2 + 2 \sum_{s=0}^{n-1} \frac{1}{(s + 1)^{c - 1}} - \: . -` - -Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "pullCount"}[]. -::: - -:::proof "expectation_pullCount_le" - Uses: {uses "some_sum_eq_zero"}[], {uses "prob_ucbIndex_le"}[], {uses "pullCount_basic"}[], {uses "pullCount_le_add_three"}[] -::: - - -:::lemma_ "ucb_regret_le" (parent := "banditAlgorithms") (lean := "Bandits.UCB.regret_le") -Suppose that $`\nu(a)` is $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] for all arms $`a \in [K]`. -For the {uses "ucbAlgorithm"}[UCB algorithm] with parameter $`c \sigma^2 > 0`, for any time $`n \in \mathbb{N}`, we have -$$` - P[R_n] - \le \sum_{a : \Delta_a > 0} \left(\frac{8 c \sigma^2 \log(n + 1)}{\Delta_a} + 2 \Delta_a\left(1 + \sum_{s=0}^{n-1} \frac{1}{(s + 1)^{c - 1}}\right)\right) - \: . -` - -Uses: {uses "stationaryEnv"}[], {uses "regret"}[], {uses "IsAlgEnvSeq"}[], {uses "gap"}[]. -::: - -:::proof "ucb_regret_le" - Uses: {uses "integral_regret_eq_sum_mul"}[], {uses "pullCount_basic"}[], {uses "expectation_pullCount_le"}[] -::: - -TODO: for $`c > 2`, the sum converges to a constant, so we get a logarithmic regret bound. diff --git a/verso_blueprint/LMLBlueprint/Chapters/Concentration.lean b/verso_blueprint/LMLBlueprint/Chapters/Concentration.lean deleted file mode 100644 index 21ed82c3..00000000 --- a/verso_blueprint/LMLBlueprint/Chapters/Concentration.lean +++ /dev/null @@ -1,189 +0,0 @@ -import Verso -import VersoManual -import VersoBlueprint -import LeanMachineLearning.SequentialLearning.Deterministic -import LeanMachineLearning.SequentialLearning.FiniteActions -import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace -import LeanMachineLearning.SequentialLearning.StationaryEnv -import LeanMachineLearning.Online.Bandit.ArrayProbSpace -import LeanMachineLearning.Online.Bandit.Regret -import LeanMachineLearning.Online.Bandit.RewardByCountMeasure -import LeanMachineLearning.Online.Bandit.SumRewards -import LeanMachineLearning.Probability.Moments.SubGaussian -import LMLBlueprint.References -import LMLBlueprint.TeXPrelude -import Mathlib.Probability.Moments.SubGaussian - -open Verso.Genre -open Verso.Genre.Manual -open Informal - -#doc (Manual) "Concentration inequalities" => - -# Sub-Gaussian random variables - -:::group "subGaussian" -Sub-Gaussian random variables -::: - -:::definition "subGaussian" (parent := "subGaussian") (lean := "ProbabilityTheory.HasSubgaussianMGF") -A real valued random variable $`X` is $`\sigma^2`-sub-Gaussian if for any $`\lambda \in \mathbb{R}`, -$$` - P\left[e^{\lambda X}\right] - \le e^{\frac{\lambda^2 \sigma^2}{2}} - \: . -` -::: - - -:::lemma_ "subGaussian_add_of_indepFun" (parent := "subGaussian") (lean := "ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun") -If $`X` is $`\sigma_1^2`-{uses "subGaussian"}[sub-Gaussian] and $`Y` is $`\sigma_2^2`-sub-Gaussian, and $`X` and $`Y` are independent, then $`X + Y` is $`(\sigma_1^2 + \sigma_2^2)`-sub-Gaussian. -::: - - -:::lemma_ "hoeffding_one" (parent := "subGaussian") (lean := "ProbabilityTheory.HasSubgaussianMGF.measure_ge_le") -For $`X` a $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] random variable, for any $`t \ge 0`, -$$` - P(X \ge t) - \le \exp\left(- \frac{t^2}{2 \sigma^2}\right) - \: . -` -::: - - -:::theorem "hoeffding" (parent := "subGaussian") (lean := "ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun") -Let $`X_1, \ldots, X_n` be independent random variables such that $`X_i` is $`\sigma_i^2`-{uses "subGaussian"}[sub-Gaussian] for $`i \in [n]`. -Then for any $`t \ge 0`, -$$` - P\left(\sum_{i=1}^n X_i \ge t\right) - \le \exp\left(- \frac{t^2}{2 \sum_{i=1}^n \sigma_i^2}\right) - \: . -` -::: - -:::proof "hoeffding" -Uses: {uses "subGaussian_add_of_indepFun"}[], {uses "hoeffding_one"}[]. -::: - - -:::lemma_ "measure_sum_le_sum_le'" (parent := "subGaussian") -Let $`X_1, \ldots, X_n` be random variables such that $`X_i - P[X_i]` is $`\sigma_{X,i}^2`-{uses "subGaussian"}[sub-Gaussian] for $`i \in [n]`. -Let $`Y_1, \ldots, Y_m` be random variables such that $`Y_i - P[Y_i]` is $`\sigma_{Y,i}^2`-{uses "subGaussian"}[sub-Gaussian] for $`i \in [m]`. -Suppose further that the vectors $`X` and $`Y` are independent and that $`\sum_{i = 1}^m P[Y_i] \le \sum_{i = 1}^n P[X_i]`. -Then -$$` - P\left(\sum_{i=1}^m Y_i \ge \sum_{i=1}^n X_i\right) - \le \exp\left(- \frac{\left(\sum_{i = 1}^n P[X_i] - \sum_{i=1}^m P[Y_i]\right)^2}{2 \sum_{i=1}^n (\sigma_{X,i}^2 + \sigma_{Y,i}^2)}\right) - \: . -` - -This is "ProbabilityTheory.HasSubgaussianMGF.measure\_sum\_le\_sum\_le'" in Lean, but I get a strange error if I add that information. -::: - -:::proof "measure_sum_le_sum_le'" -Uses: {uses "subGaussian_add_of_indepFun"}[], {uses "hoeffding_one"}[]. -::: - - - -# Concentration of the sums of rewards in bandit models - -:::group "concentrationBandits" -Concentration of the sums of rewards in bandit models -::: - -:::lemma_ "identDistrib_pullCount_prod_sumRewards" (parent := "concentrationBandits") (lean := "Bandits.ArrayModel.identDistrib_pullCount_prod_sumRewards") -In the array model, for $`t \in \mathbb{N}`, the random variable $`(N_{t,a}, S_{t, a})_{a \in \mathcal{A}}` has the same distribution as $`(N_{t,a}, \sum_{s=0}^{N_{t,a}-1} \omega_{2, s, a})_{a \in \mathcal{A}}`. - -Uses: {uses "arrayMeasure"}[] ,{uses "AM.history"}[], {uses "algorithm"}[], {uses "sumRewards"}[], {uses "pullCount"}[]. -::: - -:::proof "identDistrib_pullCount_prod_sumRewards" -Uses: {uses "AM.history"}[], {uses "stepsUntil_basic"}[], {uses "ionescu-tulcea"}[], {uses "algFunction"}[], {uses "AM.measurable_hist"}[], {uses "rewardByCount"}[], {uses "pullCount_basic"}[], {uses "stepsUntil"}[], {uses "sum_rewardByCount"}[]. -::: - - -:::lemma_ "AM.identDistrib_sum_range_snd" (parent := "concentrationBandits") (lean := "Bandits.ArrayModel.identDistrib_sum_range_snd") -In the {uses "arrayMeasure"}[array model], for $`k \in \mathbb{N}`, the random variable $`\sum_{s=0}^{k-1} \omega_{2, s, a}` has the same distribution as a sum of $`k` i.i.d. random variables with law $`\nu(a)`. -::: - -:::proof "AM.identDistrib_sum_range_snd" -By definition of {uses "arrayMeasure"}[$`P_{\mathcal{A}}`]. -::: - - -:::lemma_ "prob_pullCount_prod_sumRewards_mem_le" (parent := "concentrationBandits") (lean := "Bandits.ArrayModel.prob_pullCount_prod_sumRewards_mem_le, Bandits.prob_pullCount_prod_sumRewards_mem_le") -In the {uses "arrayMeasure"}[array model], for $`t \in \mathbb{N}`, $`a \in \mathcal{A}`, and a measurable set $`B \subseteq \mathbb{N} \times \mathbb{R}`, -$$` - P_{\mathcal{A}}\left((N_{t,a}, S_{t, a}) \in B\right) - \le \sum_{k < t, \exists r, (k, r) \in B} \nu(a)^{\otimes \mathbb{N}} \left(\sum_{s=0}^{k-1} \omega_{s} \in \{x \mid \exists n, (n, x) \in B\}\right) - \: . -` -As a consequence, this also holds for any algorithm-environment sequence. - -Uses: {uses "AM.history"}[], {uses "sumRewards"}[], {uses "pullCount"}[], {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[]. -::: - -:::proof "prob_pullCount_prod_sumRewards_mem_le" - Uses: {uses "AM.identDistrib_sum_range_snd"}[], {uses "identDistrib_pullCount_prod_sumRewards"}[], {uses "AM.measurable_hist"}[], {uses "pullCount_basic"}[], {uses "isAlgEnvSeq_arrayMeasure"}[], {uses "AM.measurable_hist"}[], {uses "isAlgEnvSeq_unique"}[] -::: - - -:::lemma_ "prob_sumRewards_le_sumRewards_le" (parent := "concentrationBandits") (lean := "Bandits.ArrayModel.prob_sumRewards_le_sumRewards_le, Bandits.probReal_sumRewards_le_sumRewards_le") -In the array model, -$$` - P_{\mathcal{A}}\left( N_{t, a^*} = m_1 \wedge N_{t, a} = m_2 \wedge S_{t, a^*} \le S_{t, a}\right) - \le (\otimes_a \nu(a))^{\otimes \mathbb{N}} \left( \sum_{s=0}^{m_1-1} \omega_{s, a^*} \le \sum_{s=0}^{m_2-1} \omega_{s, a} \right) - \: . -` -As a consequence, this also holds for any algorithm-environment sequence. - -Uses: {uses "AM.history"}[], {uses "sumRewards"}[], {uses "pullCount"}[], {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[] -::: - -:::proof "prob_sumRewards_le_sumRewards_le" - Uses: {uses "identDistrib_pullCount_prod_sumRewards"}[], {uses "AM.measurable_hist"}[], {uses "pullCount_basic"}[], {uses "isAlgEnvSeq_arrayMeasure"}[], {uses "AM.measurable_hist"}[], {uses "isAlgEnvSeq_unique"}[] -::: - - - -## Sub-Gaussian rewards - -:::lemma_ "probReal_sum_le_sum_streamMeasure" (parent := "concentrationBandits") (lean := "Bandits.probReal_sum_le_sum_streamMeasure") -Let $`\nu(a)` be a $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] distribution on $`\mathbb{R}` for each arm $`a \in \mathcal{A}`. -$$` - (\otimes_a \nu(a))^{\otimes \mathbb{N}} \left( \sum_{s=0}^{m-1} \omega_{s, a^*} \le \sum_{s=0}^{m-1} \omega_{s, a} \right) - \le \exp\left( -m \frac{\Delta_a^2}{4 \sigma^2} \right) -` - -Uses: {uses "ionescu-tulcea"}[], {uses "gap"}[] -::: - -:::proof "probReal_sum_le_sum_streamMeasure" - Uses: {uses "measure_sum_le_sum_le'"}[] -::: - - -:::lemma_ "prob_sum_le_sqrt_log" (parent := "concentrationBandits") (lean := "Bandits.prob_sum_le_sqrt_log, Bandits.prob_sum_ge_sqrt_log") -Let $`\nu(a)` be a $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] distribution on $`\mathbb{R}` for each arm $`a \in \mathcal{A}`. -Let $`c \ge 0` be a real number and $`k` a positive natural number. -Then -$$` - \nu(a)^{\otimes \mathbb{N}} \left( \sum_{s=0}^{k-1} (\omega_{s} - \mu_a) \le - \sqrt{2 c k \sigma^2 \log(n + 1)} \right) - \le \frac{1}{(n + 1)^{c}} - \: . -` - -The same upper bound holds for the upper tail: -$$` - \nu(a)^{\otimes \mathbb{N}} \left( \sum_{s=0}^{k-1} (\omega_{s} - \mu_a) \ge \sqrt{2 c k \sigma^2 \log(n + 1)} \right) - \le \frac{1}{(n + 1)^{c}} - \: . -` - -Uses: {uses "ionescu-tulcea"}[] -::: - -:::proof "prob_sum_le_sqrt_log" - Uses: {uses "hoeffding"}[]. -::: diff --git a/verso_blueprint/LMLBlueprint/Chapters/Intro.lean b/verso_blueprint/LMLBlueprint/Chapters/Intro.lean deleted file mode 100644 index ced3462c..00000000 --- a/verso_blueprint/LMLBlueprint/Chapters/Intro.lean +++ /dev/null @@ -1,36 +0,0 @@ -import Verso -import VersoManual -import VersoBlueprint - -open Verso.Genre -open Verso.Genre.Manual -open Informal - -#doc (Manual) "Introduction" => -%%% -htmlSplit := .never -%%% - -A bandit algorithm sequentially chooses actions and then observes rewards, whose distribution depends on the action chosen. -The algorithm does not know the distribution of the rewards and sees only a reward from the chosen action at any given time. -A key part of the interaction is that the algorithm can choose the next action based on all the previous actions and rewards. -The goal of the algorithm is typically to maximize the cumulative reward over time. -The researcher studying bandit algorithms is interested in the performance of the algorithm, which is measured by the _regret_ $`R_T` after choosing $`T` actions, that is the difference between the cumulative reward of always playing the best action and the cumulative reward of the algorithm. -A theoretical guarantee will be of the form $`\mathbb{E}[R_T] \le f(T)` for some function $`f`. -Here the expectation is taken over the randomness of the algorithm and the rewards. -In parallel to the theoretical study, the researcher may also be interested in the practical performance of the algorithm, which is usually measured by the average regret over several runs of the algorithm with rewards sampled from standard probability distributions. - -From that description, we highlight three key components of research work on bandit algorithms: -- A bandit algorithm is both a subject of theoretical study and a practical tool, that we should be able to implement and run, -- the bandit model defines a probability space, on which we want to take expectations, and the theoretical study deals with random variables on that space using tools like concentration inequalities, -- for the experimental part, we need to be able to sample rewards from a range of probability distributions. - -# Notations - -$`P(E)` is the probability of event $`E` under the probability distribution $`P`. - -$`P[X]` is the expectation of random variable $`X`. - -$`P[X \mid Y]` is the conditional expectation of random variable $`X` given random variable $`Y`. - -$`P(X \mid Y)` is the conditional distribution of random variable $`X` given random variable $`Y`. diff --git a/verso_blueprint/LMLBlueprint/References.lean b/verso_blueprint/LMLBlueprint/References.lean deleted file mode 100644 index 61f45e1e..00000000 --- a/verso_blueprint/LMLBlueprint/References.lean +++ /dev/null @@ -1,24 +0,0 @@ -import VersoManual.Bibliography -import VersoBlueprint.Cite - -open Verso.Genre.Manual -open Verso.Genre.Manual.Bibliography - -@[bib "lattimore2020bandit"] -def lattimore2020bandit : Verso.Genre.Manual.Bibliography.Citable := .article { - title := inlines!"Bandit algorithms" - authors := #[inlines!"Tor Lattimore", inlines!"Csaba Szepesvári"] - year := 2020 - journal := inlines!"Cambridge University Press" - month := none - volume := inlines!"0" - number := inlines!"0" -} - -@[bib "marion2025formalization"] -def marion2025formalization : Verso.Genre.Manual.Bibliography.Citable := .arXiv { - title := inlines!"A Formalization of the Ionescu-Tulcea Theorem in Mathlib" - authors := #[inlines!"Etienne Marion"] - year := 2025 - id := "2506.18616" -} diff --git a/verso_blueprint/LMLBlueprint/TeXPrelude.lean b/verso_blueprint/LMLBlueprint/TeXPrelude.lean deleted file mode 100644 index 92f0bc1e..00000000 --- a/verso_blueprint/LMLBlueprint/TeXPrelude.lean +++ /dev/null @@ -1,8 +0,0 @@ -import Verso -import VersoManual -import VersoBlueprint - -open Informal - -tex_prelude - r#"\providecommand{\ind}{\perp\!\!\!\!\perp}"# diff --git a/verso_blueprint/Main.lean b/verso_blueprint/Main.lean deleted file mode 100644 index f9acc76c..00000000 --- a/verso_blueprint/Main.lean +++ /dev/null @@ -1,25 +0,0 @@ -import VersoManual -import VersoBlueprint.PreviewManifest -import LMLBlueprint.Blueprint - -open Verso Doc -open Verso.Genre Manual Verso.Output.Html - - -def extraHead : Array Verso.Output.Html := #[ - {{}}, - {{}}, -] - -def config : RenderConfig := { - extraHead := extraHead, - sourceLink := some "https://github.com/LeanMachineLearning/LML", - issueLink := some "https://github.com/LeanMachineLearning/LML/issues", -} - -def main (args : List String) : IO UInt32 := - Informal.PreviewManifest.manualMainWithSharedPreviewManifest - (%doc LMLBlueprint.Blueprint) - args - (extensionImpls := by exact extension_impls%) - (config := config) diff --git a/verso_blueprint/lake-manifest.json b/verso_blueprint/lake-manifest.json deleted file mode 100644 index 640b9b3a..00000000 --- a/verso_blueprint/lake-manifest.json +++ /dev/null @@ -1,163 +0,0 @@ -{"version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": - [{"type": "path", - "scope": "", - "name": "LeanMachineLearning", - "manifestFile": "lake-manifest.json", - "inherited": false, - "dir": "../", - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/verso-blueprint", - "type": "git", - "subDir": null, - "scope": "", - "rev": "11c82ed5b84417b0aecc4a22b89ee536ee832ff4", - "name": "VersoBlueprint", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/mathlib4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "1ccad003f48319848becd773bde09f17729eec3e", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "1ccad003f48319848becd773bde09f17729eec3e", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/verso", - "type": "git", - "subDir": null, - "scope": "", - "rev": "4c6b02ee232211811f9ad1c148ac336122e256d7", - "name": "verso", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "1537e3fc7e680d64e06fe5fb95c4c9edee7941c2", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/verso-slides.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "2b5ce1ffa9f22743057068128e20aee96a798976", - "name": "«verso-slides»", - "manifestFile": "lake-manifest.json", - "inputRev": "2b5ce1ffa9f22743057068128e20aee96a798976", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "744117af710b1c0400cd297c9ce91f8d0ad3a347", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", - "name": "LeanSearchClient", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "99c763c8a96d3d44fb4994e96eaa51ca4568449d", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "7897ea6e5cfc6522d355083bdfa798377ab35e11", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "94346b7b49c36ae871639d1434232f057c193d60", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "5dd219c775e402f818b42cd3997b5cf21017babf", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/illuminate", - "type": "git", - "subDir": null, - "scope": "", - "rev": "c7a8de81e102ee2a42a7395f98d1ed12a861a43b", - "name": "illuminate", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/subverso", - "type": "git", - "subDir": null, - "scope": "", - "rev": "a86770a5eba721c8554d1d7fce741bc4dde3bb61", - "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": "baf3e62fbb3502305076ca077e004aea78157c63", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0-rc2", - "inherited": true, - "configFile": "lakefile.toml"}], - "name": "LMLBlueprint", - "lakeDir": ".lake", - "fixedToolchain": false} diff --git a/verso_blueprint/lakefile.lean b/verso_blueprint/lakefile.lean deleted file mode 100644 index c08d41ab..00000000 --- a/verso_blueprint/lakefile.lean +++ /dev/null @@ -1,15 +0,0 @@ -import Lake -open Lake DSL - -require VersoBlueprint from git "https://github.com/leanprover/verso-blueprint"@"v4.30.0" -require LeanMachineLearning from "../" - -package LMLBlueprint where - precompileModules := false - leanOptions := #[⟨`experimental.module, true⟩] - -@[default_target] -lean_lib LMLBlueprint where - -lean_exe «blueprint-gen» where - root := `Main diff --git a/verso_blueprint/lean-toolchain b/verso_blueprint/lean-toolchain deleted file mode 100644 index 6af09a89..00000000 --- a/verso_blueprint/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:v4.31.0-rc2 \ No newline at end of file diff --git a/verso_blueprint/scripts/ci-pages.sh b/verso_blueprint/scripts/ci-pages.sh deleted file mode 100644 index 0d1309e7..00000000 --- a/verso_blueprint/scripts/ci-pages.sh +++ /dev/null @@ -1,10 +0,0 @@ -#!/usr/bin/env bash - - -lake build -lake exe blueprint-gen --output _out/site -mkdir -p _out/site/html-multi/static -cp static_files/* _out/site/html-multi/static - -test -f _out/site/html-multi/index.html -test -f _out/site/html-multi/-verso-data/blueprint-preview-manifest.json diff --git a/verso_blueprint/static_files/LigaMenlo-Regular.ttf b/verso_blueprint/static_files/LigaMenlo-Regular.ttf deleted file mode 100644 index b1ca21e2..00000000 Binary files a/verso_blueprint/static_files/LigaMenlo-Regular.ttf and /dev/null differ diff --git a/verso_blueprint/static_files/favicon.svg b/verso_blueprint/static_files/favicon.svg deleted file mode 100644 index ea497ae3..00000000 --- a/verso_blueprint/static_files/favicon.svg +++ /dev/null @@ -1 +0,0 @@ -RealFaviconGeneratorhttps://realfavicongenerator.net \ No newline at end of file diff --git a/verso_blueprint/static_files/scripts.js b/verso_blueprint/static_files/scripts.js deleted file mode 100644 index 64c37a8d..00000000 --- a/verso_blueprint/static_files/scripts.js +++ /dev/null @@ -1,23 +0,0 @@ -window.addEventListener('load', function () { - document.querySelectorAll('.has-info, .warning').forEach(function (el) { - el.classList.remove('has-info', 'warning'); - - el.querySelectorAll('span.hover-container').forEach(function (hoverSpan) { - hoverSpan.remove(); - }); - }); - - document.querySelectorAll('p').forEach(function (p) { - if (p.querySelector('img')) { - p.setAttribute('align', 'center'); - } - }); - - document.querySelectorAll('a[href]').forEach(function (link) { - const url = new URL(link.href, window.location.href); - if (url.hostname !== window.location.hostname) { - link.setAttribute('target', '_blank'); - link.setAttribute('rel', 'noopener noreferrer'); - } - }); -}); diff --git a/verso_blueprint/static_files/style.css b/verso_blueprint/static_files/style.css deleted file mode 100644 index b329089b..00000000 --- a/verso_blueprint/static_files/style.css +++ /dev/null @@ -1,57 +0,0 @@ -:root { - --accent: #d65d5d; - --accent-compl: #e8a0a0; - --background: #fef9f9; - --background-lighter: #fefcfc; -} - -@font-face { - font-family: "LigaMenlo"; - src: url("LigaMenlo-Regular.ttf"); -} - -body { - text-align: justify; - background-color: var(--background); -} - -p a:visited, -p a:link { - text-decoration: none; - color: var(--accent); -} - -p a:hover { - text-decoration: underline; -} - -.toc { - background-color: var(--background-lighter); -} - -.keyword { - color: var(--accent) !important; -} - -.hl.lean .token.binding-hl, -.hl.lean .literal.string:hover, -.hl.lean .token.typed:hover { - background-color: var(--accent-compl) !important; - border-radius: 2px !important; -} - -.block { - background-color: var(--background-lighter); - padding: 0.4em; - border: 2px solid black; - border-radius: 0.5em; -} - -.tippy-box[data-theme~='lean'] { - background-color: var(--background-lighter) !important; -} - -code { - font-family: "LigaMenlo"; - font-variant-ligatures: normal; -}