From 5f77e9867c8930cde860f59b6eafa86c286b3b3d Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 14 Sep 2025 12:32:10 +0200 Subject: [PATCH 01/17] start description of general alg setting --- blueprint/src/chapters/probabilitySpace.tex | 33 +++++++++++++++++++++ blueprint/src/content.tex | 1 + 2 files changed, 34 insertions(+) create mode 100644 blueprint/src/chapters/probabilitySpace.tex diff --git a/blueprint/src/chapters/probabilitySpace.tex b/blueprint/src/chapters/probabilitySpace.tex new file mode 100644 index 00000000..33201fbe --- /dev/null +++ b/blueprint/src/chapters/probabilitySpace.tex @@ -0,0 +1,33 @@ +\chapter{Iterative stochastic algorithms} + + +\begin{definition}[Algorithm]\label{def:algorithm'} + \leanok + \lean{Bandits.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 pulls 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}$. + +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). + TODO etc + \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). + TODO etc + \item \textbf{Reinforcement learnings in Markov decision processes}. +\end{enumerate} + + +\section{Ionescu-Tulcea theorem} + + +\section{Independence and Markov property} diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index e0c5f9a9..ff1d7660 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -7,6 +7,7 @@ % can start with a \section or \chapter for instance. \input{chapters/intro.tex} +\input{chapters/probabilitySpace.tex} \input{chapters/bandit.tex} \input{chapters/concentration.tex} \input{chapters/etc.tex} From 5dc65c592b6208d12a9006fdcd9485ab357c39e4 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 21 Sep 2025 17:55:29 +0200 Subject: [PATCH 02/17] describe IT thm --- blueprint/lean_decls | 2 + blueprint/src/chapters/probabilitySpace.tex | 54 ++++++++++++++++++++- 2 files changed, 54 insertions(+), 2 deletions(-) diff --git a/blueprint/lean_decls b/blueprint/lean_decls index 4f0cd71a..12441e15 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -1,4 +1,6 @@ Bandits.Algorithm +ProbabilityTheory.Kernel.traj +Bandits.Algorithm Bandits.Bandit.measure Bandits.arm Bandits.reward diff --git a/blueprint/src/chapters/probabilitySpace.tex b/blueprint/src/chapters/probabilitySpace.tex index 33201fbe..996a79bd 100644 --- a/blueprint/src/chapters/probabilitySpace.tex +++ b/blueprint/src/chapters/probabilitySpace.tex @@ -19,15 +19,65 @@ \chapter{Iterative stochastic algorithms} 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). - TODO etc + 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). - TODO etc + 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 learnings 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} \section{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 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 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} + +We can then combine the kernel $\xi$ with the initial measure $\mu$ to get a probability measure $\mu \otimes \xi$ on $\prod_{i=0}^{\infty} \Omega_i$. + +TODO: the IT theorem in Mathlib 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. +Also, our actual definition of the trajectory measure is $\xi_0 \circ \mu$ due to that implementation detail. + +We denote by $\Omega_{\mathcal{T}}$ the space $\prod_{t=0}^\infty \Omega_t$ endowed with the product $\sigma$-algebra and by $\mathbb{P}_{\mathcal{T}}$ the probability measure $\mu \otimes \xi$ on that space. +The $\mathcal{T}$ subscript stands for ``trajectory''. + + +\begin{definition}\label{def:history} +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}}$. + +We now list properties of those random variables that follow from the construction of the trajectory measure. + +\begin{lemma}\label{lem:condDistrib_X_add_one} + \uses{def:history} +For any $t \in \mathbb{N}$, the conditional distribution of $X_{t+1}$ given the history $H_t$ is $P_{\mathcal{T}}$-almost surely equal to $\kappa_t$. +\end{lemma} + +\begin{proof} + +\end{proof} + \section{Independence and Markov property} + +The structure of the sequence of kernels $(\kappa_t)_{t \in \mathbb{N}}$ is reflected in independence properties of the sequence of random variables $(X_t)_{t \in \mathbb{N}}$. From d2b191390140abfbd3c72d4821c594575b42893e Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 22 Sep 2025 11:17:18 +0200 Subject: [PATCH 03/17] add bib --- blueprint/src/biblio.bib | 271 ++++++++++++++++++++ blueprint/src/chapters/probabilitySpace.tex | 7 +- blueprint/src/content.tex | 3 + 3 files changed, 277 insertions(+), 4 deletions(-) create mode 100644 blueprint/src/biblio.bib diff --git a/blueprint/src/biblio.bib b/blueprint/src/biblio.bib new file mode 100644 index 00000000..82ef848f --- /dev/null +++ b/blueprint/src/biblio.bib @@ -0,0 +1,271 @@ +@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} +} diff --git a/blueprint/src/chapters/probabilitySpace.tex b/blueprint/src/chapters/probabilitySpace.tex index 996a79bd..ffd537df 100644 --- a/blueprint/src/chapters/probabilitySpace.tex +++ b/blueprint/src/chapters/probabilitySpace.tex @@ -51,13 +51,12 @@ \section{Ionescu-Tulcea theorem} \end{theorem} We can then combine the kernel $\xi$ with the initial measure $\mu$ to get a probability measure $\mu \otimes \xi$ on $\prod_{i=0}^{\infty} \Omega_i$. - -TODO: the IT theorem in Mathlib 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. -Also, our actual definition of the trajectory measure is $\xi_0 \circ \mu$ due to that implementation detail. - We denote by $\Omega_{\mathcal{T}}$ the space $\prod_{t=0}^\infty \Omega_t$ endowed with the product $\sigma$-algebra and by $\mathbb{P}_{\mathcal{T}}$ the probability measure $\mu \otimes \xi$ on that space. The $\mathcal{T}$ subscript stands for ``trajectory''. +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. +Due to that implementation, our actual definition of the trajectory measure is $\xi_0 \circ \mu$. + \begin{definition}\label{def:history} 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$. diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index ff1d7660..3fc097c5 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -14,3 +14,6 @@ \input{chapters/ucb.tex} \input{chapters/practicalAlgorithms.tex} \input{chapters/sampling.tex} + +\bibliographystyle{amsalpha} +\bibliography{biblio} From 315d53f72a7a09031d41b30617fd2a19eb707a31 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 22 Sep 2025 11:38:08 +0200 Subject: [PATCH 04/17] add defs --- blueprint/lean_decls | 2 ++ blueprint/src/chapters/probabilitySpace.tex | 25 +++++++++++++++------ 2 files changed, 20 insertions(+), 7 deletions(-) diff --git a/blueprint/lean_decls b/blueprint/lean_decls index 12441e15..8e326cca 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -1,5 +1,7 @@ Bandits.Algorithm ProbabilityTheory.Kernel.traj +ProbabilityTheory.Kernel.trajMeasure +ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel Bandits.Algorithm Bandits.Bandit.measure Bandits.arm diff --git a/blueprint/src/chapters/probabilitySpace.tex b/blueprint/src/chapters/probabilitySpace.tex index ffd537df..9a20e833 100644 --- a/blueprint/src/chapters/probabilitySpace.tex +++ b/blueprint/src/chapters/probabilitySpace.tex @@ -50,15 +50,23 @@ \section{Ionescu-Tulcea theorem} 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} -We can then combine the kernel $\xi$ with the initial measure $\mu$ to get a probability measure $\mu \otimes \xi$ on $\prod_{i=0}^{\infty} \Omega_i$. -We denote by $\Omega_{\mathcal{T}}$ the space $\prod_{t=0}^\infty \Omega_t$ endowed with the product $\sigma$-algebra and by $\mathbb{P}_{\mathcal{T}}$ the probability measure $\mu \otimes \xi$ on that space. -The $\mathcal{T}$ subscript stands for ``trajectory''. +\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. -Due to that implementation, our actual definition of the trajectory measure is $\xi_0 \circ \mu$. + +\begin{definition}\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}\label{def:history} + \leanok % no need for a Lean definition 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} @@ -67,12 +75,15 @@ \section{Ionescu-Tulcea theorem} We now list properties of those random variables that follow from the construction of the trajectory measure. + \begin{lemma}\label{lem:condDistrib_X_add_one} - \uses{def:history} -For any $t \in \mathbb{N}$, the conditional distribution of $X_{t+1}$ given the history $H_t$ is $P_{\mathcal{T}}$-almost surely equal to $\kappa_t$. + \uses{def:history, def:trajMeasure} + \leanok + \lean{ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel} +For any $t \in \mathbb{N}$, the conditional distribution of $X_{t+1}$ given the history $H_t$ as a function $\prod_{s=0}^t \Omega_s \to \Omega_{t+1}$ is $(\pi_{[1,t+1]*} P_{\mathcal{T}})$-almost surely equal to $\kappa_t$. \end{lemma} -\begin{proof} +\begin{proof}\leanok \end{proof} From 20236a4695c95aa2edf9fcc87e47b67a2da7b5a6 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 22 Sep 2025 12:41:45 +0200 Subject: [PATCH 05/17] work --- blueprint/src/chapters/probabilitySpace.tex | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/blueprint/src/chapters/probabilitySpace.tex b/blueprint/src/chapters/probabilitySpace.tex index 9a20e833..2d81e563 100644 --- a/blueprint/src/chapters/probabilitySpace.tex +++ b/blueprint/src/chapters/probabilitySpace.tex @@ -71,20 +71,23 @@ \section{Ionescu-Tulcea theorem} 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}}$. +Note: $(X_t)_{t \in \mathbb{N}}$ is the canonical process on $\Omega_{\mathcal{T}}$. $H_t$ is equal to $\pi_{[0,t]}$. We now list properties of those random variables that follow from the construction of the trajectory measure. +We write $P[X \mid Y]$ for the conditional distribution of a random variable $X$ given another random variable $Y$ under a probability measure $P$. \begin{lemma}\label{lem:condDistrib_X_add_one} \uses{def:history, def:trajMeasure} \leanok \lean{ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel} -For any $t \in \mathbb{N}$, the conditional distribution of $X_{t+1}$ given the history $H_t$ as a function $\prod_{s=0}^t \Omega_s \to \Omega_{t+1}$ is $(\pi_{[1,t+1]*} P_{\mathcal{T}})$-almost surely equal to $\kappa_t$. +For any $t \in \mathbb{N}$, the conditional distribution of $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\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} From 4720dfc997f908bb178a8a9a8d27998b69e70745 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 23 Sep 2025 17:47:57 +0200 Subject: [PATCH 06/17] blueprint: add condDistrib lemmas --- blueprint/src/chapters/probabilitySpace.tex | 76 ++++++++++++++++++++- 1 file changed, 75 insertions(+), 1 deletion(-) diff --git a/blueprint/src/chapters/probabilitySpace.tex b/blueprint/src/chapters/probabilitySpace.tex index 2d81e563..b6282ee8 100644 --- a/blueprint/src/chapters/probabilitySpace.tex +++ b/blueprint/src/chapters/probabilitySpace.tex @@ -81,7 +81,7 @@ \section{Ionescu-Tulcea theorem} \uses{def:history, def:trajMeasure} \leanok \lean{ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel} -For any $t \in \mathbb{N}$, the conditional distribution of $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t$. +For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t$. \end{lemma} \begin{proof}\leanok @@ -91,6 +91,80 @@ \section{Ionescu-Tulcea theorem} \end{proof} +\begin{lemma}\label{lem:law_X_zero} + \uses{def:history, def:trajMeasure} +The law of $X_0$ under $P_{\mathcal{T}}$ is $\mu$. +\end{lemma} + +\begin{proof} + +\end{proof} + + +\paragraph{Case of a composition-product} + +We suppose now that $\Omega_t = \mathcal{A}_t \times \mathcal{R}_t$ for some measurable spaces $\mathcal{A}_t$ and $\mathcal{R}_t$, and that for all $t \in \mathbb{N}$, $\kappa_t = \pi_t \otimes \nu_t$ for kernels $\pi_t : \prod_{s=0}^t(\mathcal{A}_s \times \mathcal{R}_s) \rightsquigarrow \mathcal{A}$ and $\nu_t : \prod_{s=0}^t(\mathcal{A}_s \times \mathcal{R}_s) \times \mathcal{A} \rightsquigarrow \mathcal{R}$. +Likewise, $\mu = \alpha_0 \otimes \nu'_0$ for a probability measure $\alpha_0$ on $\mathcal{A}_0$ and a Markov kernel $\nu'_0 : \mathcal{A}_0 \rightsquigarrow \mathcal{R}_0$. +That's the case of an algorithm interacting with an environment as described above. +We write $A_t$ and $R_t$ for the projections of $X_t$ on $\mathcal{A}_t$ and $\mathcal{R}_t$ respectively. + +\begin{lemma}\label{lem:condDistrib_A_add_one} + \uses{def:history, def:trajMeasure} +For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[A_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\pi_t$. +\end{lemma} + +\begin{proof} + \uses{lem:condDistrib_X_add_one} +By Lemma~\ref{lem:condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t = \pi_t \otimes \nu_t$. +Since $A_{t+1}$ is the projection of $X_{t+1}$ on $\mathcal{A}_{t+1}$, $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}_{t+1}$, which is $\pi_t$. +\end{proof} + + +\begin{lemma}\label{lem:condDistrib_R_add_one} + \uses{def:history, def:trajMeasure} +For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[R_{t+1} \mid H_t, A_{t+1}\right]$ is $((H_t, A_{t+1})_* P_{\mathcal{T}})$-almost surely equal to $\nu_t$. +\end{lemma} + +\begin{proof} + \uses{lem:condDistrib_X_add_one, lem: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:condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t = \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: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:law_A_zero} + \uses{def:history, def:trajMeasure} +The law of $A_0$ under $P_{\mathcal{T}}$ is $\alpha_0$. +\end{lemma} + +\begin{proof} + \uses{lem:law_X_zero} +$X_0$ has law $\mu = \alpha_0 \otimes \nu'_0$. $A_0$ is the projection of $X_0$ on the first space $\mathcal{A}_0$ and $\nu_0'$ is Markov, so $A_0$ has law $\alpha_0$. +\end{proof} + + +\begin{lemma}\label{lem:condDistrib_R_zero} + \uses{def:history, def:trajMeasure} +The conditional distribution $P_{\mathcal{T}}\left[R_0 \mid A_0\right]$ is $(A_{0*} P_{\mathcal{T}})$-almost surely equal to $\nu'_0$. +\end{lemma} + +\begin{proof} + \uses{lem:law_X_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 Lemma~\ref{lem:law_X_zero}, $X_{0*} P_{\mathcal{T}} = \mu = \alpha_0 \otimes \nu'_0$. +By Lemma~\ref{lem:law_A_zero}, $A_{0*} P_{\mathcal{T}} = \alpha_0$. +Thus the two sides are equal. +\end{proof} + + + + \section{Independence and Markov property} The structure of the sequence of kernels $(\kappa_t)_{t \in \mathbb{N}}$ is reflected in independence properties of the sequence of random variables $(X_t)_{t \in \mathbb{N}}$. From cc7197fd203c27eced17e331daf261564d6ef21e Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 23 Sep 2025 18:24:22 +0200 Subject: [PATCH 07/17] add Algorithm file --- LeanBandits.lean | 1 + LeanBandits/Algorithm.lean | 212 +++++++++++++++++++++++++++++++ LeanBandits/ForMathlib/Traj.lean | 12 ++ 3 files changed, 225 insertions(+) create mode 100644 LeanBandits/Algorithm.lean diff --git a/LeanBandits.lean b/LeanBandits.lean index aa4d81cb..ee04c0d5 100644 --- a/LeanBandits.lean +++ b/LeanBandits.lean @@ -1,3 +1,4 @@ +import LeanBandits.Algorithm import LeanBandits.AlgorithmBuilding import LeanBandits.Bandit import LeanBandits.ETC diff --git a/LeanBandits/Algorithm.lean b/LeanBandits/Algorithm.lean new file mode 100644 index 00000000..830f45f7 --- /dev/null +++ b/LeanBandits/Algorithm.lean @@ -0,0 +1,212 @@ +/- +Copyright (c) 2025 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne, Paulo Rauber +-/ +import Mathlib +import LeanBandits.ForMathlib.CondDistrib +import LeanBandits.ForMathlib.KernelCompositionLemmas +import LeanBandits.ForMathlib.Traj + +/-! +# Bandit +-/ + +open MeasureTheory ProbabilityTheory Filter Real Finset + +open scoped ENNReal NNReal + +namespace Learning + +variable {α R : Type*} {mα : MeasurableSpace α} {mR : MeasurableSpace R} + +/-- A stochastic, sequential algorithm. -/ +structure Algorithm (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] where + /-- Policy or sampling rule: distribution of the next action. -/ + policy : (n : ℕ) → Kernel (Iic n → α × R) α + [h_policy : ∀ n, IsMarkovKernel (policy n)] + /-- Distribution of the first action. -/ + p0 : Measure α + [hp0 : IsProbabilityMeasure p0] + +instance (alg : Algorithm α R) (n : ℕ) : IsMarkovKernel (alg.policy n) := alg.h_policy n +instance (alg : Algorithm α R) : IsProbabilityMeasure alg.p0 := alg.hp0 + +/-- A stochastic environment. -/ +structure Environment (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] where + /-- Distribution of the next observation as function of the past history. -/ + feedback : (n : ℕ) → Kernel ((Iic n → α × R) × α) R + [h_feedback : ∀ n, IsMarkovKernel (feedback n)] + /-- Distribution of the first observation given the first action. -/ + ν0 : Kernel α R + [hp0 : IsMarkovKernel ν0] + +instance (env : Environment α R) (n : ℕ) : IsMarkovKernel (env.feedback n) := env.h_feedback n +instance (env : Environment α R) : IsMarkovKernel env.ν0 := env.hp0 + +/-- A deterministic algorithm. -/ +noncomputable +def detAlgorithm (nextaction : (n : ℕ) → (Iic n → α × R) → α) + (h_next : ∀ n, Measurable (nextaction n)) (action0 : α) : + Algorithm α R where + policy n := Kernel.deterministic (nextaction n) (h_next n) + p0 := Measure.dirac action0 + +/-- A stationary environment, in which the distribution of the next reward depends only on the last +action. -/ +def stationaryEnv (ν : Kernel α R) (n : ℕ) : Kernel ((Iic n → α × R) × α) R := ν.prodMkLeft _ + +/-- Kernel describing the distribution of the next action-reward pair given the history +up to `n`. -/ +noncomputable +def stepKernel (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : + Kernel (Iic n → α × R) (α × R) := + alg.policy n ⊗ₖ env.feedback n +deriving IsMarkovKernel + +@[simp] +lemma fst_stepKernel (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : + (stepKernel alg env n).fst = alg.policy n := by + rw [stepKernel, Kernel.fst_compProd] + +/-- Kernel sending a partial trajectory of the bandit interaction `Iic n → α × ℝ` to a measure +on `ℕ → α × ℝ`, supported on full trajectories that start with the partial one. -/ +noncomputable def traj (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : + Kernel (Iic n → α × R) (ℕ → α × R) := + ProbabilityTheory.Kernel.traj (X := fun _ ↦ α × R) (stepKernel alg env) n +deriving IsMarkovKernel + +/-- Measure on the sequence of actions and observations generated by the algorithm/environment. -/ +noncomputable +def trajMeasure (alg : Algorithm α R) (env : Environment α R) : + Measure (ℕ → α × R) := + Kernel.trajMeasure (alg.p0 ⊗ₘ env.ν0) (stepKernel alg env) +deriving IsProbabilityMeasure + +/-- Action and reward at step `n`. -/ +def step (n : ℕ) (h : ℕ → α × R) : α × R := h n + +/-- `action n` is the action pulled at time `n`. This is a random variable on the measurable space +`ℕ → α × ℝ`. -/ +def action (n : ℕ) (h : ℕ → α × R) : α := (h n).1 + +/-- `reward n` is the reward at time `n`. This is a random variable on the measurable space +`ℕ → α × R`. -/ +def reward (n : ℕ) (h : ℕ → α × R) : R := (h n).2 + +/-- `hist n` is the history up to time `n`. This is a random variable on the measurable space +`ℕ → α × R`. -/ +def hist (n : ℕ) (h : ℕ → α × R) : Iic n → α × R := fun i ↦ h i + +@[fun_prop] +lemma measurable_step (n : ℕ) : Measurable (step n (α := α) (R := R)) := by + unfold step; fun_prop + +@[fun_prop] +lemma measurable_step_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ step p.1 p.2) := by + refine measurable_from_prod_countable_right fun n ↦ ?_ + simp only + fun_prop + +@[fun_prop] +lemma measurable_action (n : ℕ) : Measurable (action n (α := α) (R := R)) := by + unfold action; fun_prop + +@[fun_prop] +lemma measurable_action_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ action p.1 p.2) := by + refine measurable_from_prod_countable_right fun n ↦ ?_ + simp only + fun_prop + +@[fun_prop] +lemma measurable_reward (n : ℕ) : Measurable (reward n (α := α) (R := R)) := by + unfold reward; fun_prop + +@[fun_prop] +lemma measurable_reward_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ reward p.1 p.2) := by + refine measurable_from_prod_countable_right fun n ↦ ?_ + simp only + fun_prop + +@[fun_prop] +lemma measurable_hist (n : ℕ) : Measurable (hist n (α := α) (R := R)) := by unfold hist; fun_prop + +lemma hist_eq_frestrictLe : + hist = Preorder.frestrictLe («π» := fun _ ↦ α × R) := by + ext n h i : 3 + simp [hist, Preorder.frestrictLe] + +/-- Filtration of the algorithm interaction. -/ +protected def filtration (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] : + Filtration ℕ (inferInstance : MeasurableSpace (ℕ → α × R)) := + MeasureTheory.Filtration.piLE (X := fun _ ↦ α × R) + +lemma condDistrib_action_reward [StandardBorelSpace α] [Nonempty α] + [StandardBorelSpace R] [Nonempty R] + (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : + condDistrib (fun h ↦ (action (n + 1) h, reward (n + 1) h)) (hist n) (trajMeasure alg env) + =ᵐ[(trajMeasure alg env).map (hist n)] stepKernel alg env n := + Kernel.condDistrib_trajMeasure_ae_eq_kernel + +lemma condDistrib_action [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] + (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : + condDistrib (action (n + 1)) (hist n) (trajMeasure alg env) + =ᵐ[(trajMeasure alg env).map (hist n)] alg.policy n := by + sorry + +lemma condDistrib_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] + (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : + condDistrib (reward (n + 1)) (fun ω ↦ (hist n ω, action (n + 1) ω)) (trajMeasure alg env) + =ᵐ[(trajMeasure alg env).map (fun ω ↦ (hist n ω, action (n + 1) ω))] env.feedback n := by + sorry + +lemma hasLaw_step_zero (alg : Algorithm α R) (env : Environment α R) : + HasLaw (step 0) (alg.p0 ⊗ₘ env.ν0) (trajMeasure alg env) where + aemeasurable := Measurable.aemeasurable (by fun_prop) + map_eq := by + unfold step + simp only [trajMeasure, Kernel.trajMeasure] + rw [← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc, + Kernel.deterministic_comp_eq_map, Kernel.traj_zero_map_eval_zero, + Measure.deterministic_comp_eq_map, Measure.map_map (by fun_prop) (by fun_prop)] + simp + +lemma hasLaw_action_zero (alg : Algorithm α R) (env : Environment α R) : + HasLaw (action 0) alg.p0 (trajMeasure alg env) where + map_eq := by + have : action (α := α) (R := R) 0 = Prod.fst ∘ step 0 := rfl + rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), (hasLaw_step_zero alg env).map_eq, + ← Measure.fst, Measure.fst_compProd] + +section DetAlgorithm + +variable {nextaction : (n : ℕ) → (Iic n → α × R) → α} {h_next : ∀ n, Measurable (nextaction n)} + {action0 : α} {env : Environment α R} + +lemma HasLaw_action_zero_detAlgorithm : + HasLaw (action 0) (Measure.dirac action0) + (trajMeasure (detAlgorithm nextaction h_next action0) env) where + map_eq := (hasLaw_action_zero _ _).map_eq + +lemma action_zero_detAlgorithm [MeasurableSingletonClass α] : + action 0 =ᵐ[trajMeasure (detAlgorithm nextaction h_next action0) env] fun _ ↦ action0 := by + have h_eq : ∀ᵐ x ∂((trajMeasure (detAlgorithm nextaction h_next action0) env).map (action 0)), x + = action0 := by + rw [(hasLaw_action_zero _ _).map_eq] + simp [detAlgorithm] + exact ae_of_ae_map (by fun_prop) h_eq + +lemma action_detAlgorithm_ae_eq (n : ℕ) : + action (n + 1) =ᵐ[trajMeasure (detAlgorithm nextaction h_next action0) env] + fun h ↦ nextaction n (fun i ↦ h i) := by + sorry + +example [MeasurableSingletonClass α] : + ∀ᵐ h ∂(trajMeasure (detAlgorithm nextaction h_next action0) env), + action 0 h = action0 ∧ ∀ n, action (n + 1) h = nextaction n (fun i ↦ h i) := by + rw [eventually_and, ae_all_iff] + exact ⟨action_zero_detAlgorithm, action_detAlgorithm_ae_eq⟩ + +end DetAlgorithm + +end Learning diff --git a/LeanBandits/ForMathlib/Traj.lean b/LeanBandits/ForMathlib/Traj.lean index f8ee9d34..c50d7e81 100644 --- a/LeanBandits/ForMathlib/Traj.lean +++ b/LeanBandits/ForMathlib/Traj.lean @@ -84,4 +84,16 @@ lemma condDistrib_trajMeasure_ae_eq_kernel {a : ℕ} apply condDistrib_ae_eq_of_measure_eq_compProd₀ (by measurability) (by measurability) exact trajMeasure_map_frestrictLe_compProd_kernel_eq_trajMeasure_map.symm +lemma traj_zero_map_eval_zero : + (Kernel.traj κ 0).map (fun h ↦ h 0) + = Kernel.deterministic (MeasurableEquiv.piIicZero X) + (MeasurableEquiv.piIicZero X).measurable := by + suffices (Kernel.traj κ 0).map (fun h ↦ h 0) = (Kernel.partialTraj κ 0 0).map + (MeasurableEquiv.piIicZero X) by + rwa [Kernel.partialTraj_zero, + Kernel.deterministic_map _ (MeasurableEquiv.piIicZero X).measurable] at this + rw [← Kernel.traj_map_frestrictLe, ← Kernel.map_comp_right _ (by fun_prop) (by fun_prop)] + congr with h + sorry + end ProbabilityTheory.Kernel From 2169d3fc21b58d05c2e5641b0082c291b018b979 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 23 Sep 2025 19:55:52 +0200 Subject: [PATCH 08/17] prove condDistrib_reward --- LeanBandits/Algorithm.lean | 25 ++++++++++++++------- LeanBandits/Bandit.lean | 23 +------------------ LeanBandits/ForMathlib/CondDistrib.lean | 11 +++++++++ blueprint/lean_decls | 3 +++ blueprint/src/chapters/probabilitySpace.tex | 13 ++++++++--- 5 files changed, 42 insertions(+), 33 deletions(-) diff --git a/LeanBandits/Algorithm.lean b/LeanBandits/Algorithm.lean index 830f45f7..1daed91d 100644 --- a/LeanBandits/Algorithm.lean +++ b/LeanBandits/Algorithm.lean @@ -98,6 +98,8 @@ def reward (n : ℕ) (h : ℕ → α × R) : R := (h n).2 `ℕ → α × R`. -/ def hist (n : ℕ) (h : ℕ → α × R) : Iic n → α × R := fun i ↦ h i +lemma fst_comp_step (n : ℕ) : Prod.fst ∘ step (α := α) (R := R) n = action n := rfl + @[fun_prop] lemma measurable_step (n : ℕ) : Measurable (step n (α := α) (R := R)) := by unfold step; fun_prop @@ -141,10 +143,9 @@ protected def filtration (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] Filtration ℕ (inferInstance : MeasurableSpace (ℕ → α × R)) := MeasureTheory.Filtration.piLE (X := fun _ ↦ α × R) -lemma condDistrib_action_reward [StandardBorelSpace α] [Nonempty α] - [StandardBorelSpace R] [Nonempty R] +lemma condDistrib_step [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : - condDistrib (fun h ↦ (action (n + 1) h, reward (n + 1) h)) (hist n) (trajMeasure alg env) + condDistrib (step (n + 1)) (hist n) (trajMeasure alg env) =ᵐ[(trajMeasure alg env).map (hist n)] stepKernel alg env n := Kernel.condDistrib_trajMeasure_ae_eq_kernel @@ -152,13 +153,22 @@ lemma condDistrib_action [StandardBorelSpace α] [Nonempty α] [StandardBorelSpa (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : condDistrib (action (n + 1)) (hist n) (trajMeasure alg env) =ᵐ[(trajMeasure alg env).map (hist n)] alg.policy n := by - sorry + rw [← fst_comp_step] + refine (condDistrib_comp' (by fun_prop) (by fun_prop) (by fun_prop)).trans ?_ + filter_upwards [condDistrib_step alg env n] with h h_eq + rw [Kernel.map_apply _ (by fun_prop), h_eq, ← Kernel.map_apply _ (by fun_prop), ← Kernel.fst_eq, + fst_stepKernel] lemma condDistrib_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : condDistrib (reward (n + 1)) (fun ω ↦ (hist n ω, action (n + 1) ω)) (trajMeasure alg env) =ᵐ[(trajMeasure alg env).map (fun ω ↦ (hist n ω, action (n + 1) ω))] env.feedback n := by - sorry + have h_step := condDistrib_step alg env n + have h_action := condDistrib_action alg env n + rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)] at h_step h_action ⊢ + rw [h_action, Measure.compProd_assoc, ← stepKernel, ← h_step, + Measure.map_map (by fun_prop) (by fun_prop)] + rfl lemma hasLaw_step_zero (alg : Algorithm α R) (env : Environment α R) : HasLaw (step 0) (alg.p0 ⊗ₘ env.ν0) (trajMeasure alg env) where @@ -174,9 +184,8 @@ lemma hasLaw_step_zero (alg : Algorithm α R) (env : Environment α R) : lemma hasLaw_action_zero (alg : Algorithm α R) (env : Environment α R) : HasLaw (action 0) alg.p0 (trajMeasure alg env) where map_eq := by - have : action (α := α) (R := R) 0 = Prod.fst ∘ step 0 := rfl - rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), (hasLaw_step_zero alg env).map_eq, - ← Measure.fst, Measure.fst_compProd] + rw [← fst_comp_step, ← Measure.map_map (by fun_prop) (by fun_prop), + (hasLaw_step_zero alg env).map_eq, ← Measure.fst, Measure.fst_compProd] section DetAlgorithm diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index 517debd5..7947f669 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -147,27 +147,6 @@ protected def filtration (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] Filtration ℕ (inferInstance : MeasurableSpace (ℕ → α × R)) := MeasureTheory.Filtration.piLE (X := fun _ ↦ α × R) -section Traj - -open Kernel Preorder - -variable {X : ℕ → Type*} [∀ n, MeasurableSpace (X n)] - {κ : (n : ℕ) → Kernel ((i : { x // x ∈ Iic n }) → X i) (X (n + 1))} [∀ n, IsMarkovKernel (κ n)] - -lemma traj_zero_map_eval_zero : - (Kernel.traj κ 0).map (fun h ↦ h 0) - = Kernel.deterministic (MeasurableEquiv.piIicZero X) - (MeasurableEquiv.piIicZero X).measurable := by - suffices (Kernel.traj κ 0).map (fun h ↦ h 0) = (Kernel.partialTraj κ 0 0).map - (MeasurableEquiv.piIicZero X) by - rwa [Kernel.partialTraj_zero, - Kernel.deterministic_map _ (MeasurableEquiv.piIicZero X).measurable] at this - rw [← Kernel.traj_map_frestrictLe, ← Kernel.map_comp_right _ (by fun_prop) (by fun_prop)] - congr with h - sorry - -end Traj - lemma condDistrib_arm_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : condDistrib (fun h ↦ (arm (n + 1) h, reward (n + 1) h)) (hist n) (Bandit.trajMeasure alg ν) @@ -199,7 +178,7 @@ lemma hasLaw_step_zero map_eq := by simp only [Bandit.trajMeasure, Kernel.trajMeasure] rw [← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc, - Kernel.deterministic_comp_eq_map, traj_zero_map_eval_zero, + Kernel.deterministic_comp_eq_map, Kernel.traj_zero_map_eval_zero, Measure.deterministic_comp_eq_map, Measure.map_map (by fun_prop) (by fun_prop)] simp diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean index baf7bb06..d38ff220 100644 --- a/LeanBandits/ForMathlib/CondDistrib.lean +++ b/LeanBandits/ForMathlib/CondDistrib.lean @@ -399,6 +399,17 @@ lemma condDistrib_ae_eq_iff_measure_eq_compProd₀ refine ⟨fun h ↦ ?_, condDistrib_ae_eq_of_measure_eq_compProd₀ hX hY κ⟩ rw [Measure.compProd_congr h.symm, compProd_map_condDistrib hY] +lemma condDistrib_comp' (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) + {f : Ω → Ω'} (hf : Measurable f) : + condDistrib (f ∘ Y) X μ =ᵐ[μ.map X] (condDistrib Y X μ).map f := by + refine condDistrib_ae_eq_of_measure_eq_compProd₀ hX (by fun_prop) _ ?_ + calc μ.map (fun x ↦ (X x, (f ∘ Y) x)) + _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ μ.map (fun x ↦ (X x, Y x)) := by + sorry + _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (μ.map X ⊗ₘ condDistrib Y X μ) := by + rw [compProd_map_condDistrib hY] + _ = μ.map X ⊗ₘ (condDistrib Y X μ).map f := sorry + lemma condDistrib_comp (hX : AEMeasurable X μ) {f : β → Ω} (hf : Measurable f) : condDistrib (f ∘ X) X μ =ᵐ[μ.map X] Kernel.deterministic f hf := by refine condDistrib_ae_eq_of_measure_eq_compProd₀ hX (by fun_prop) _ ?_ diff --git a/blueprint/lean_decls b/blueprint/lean_decls index 8e326cca..883c158e 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -2,6 +2,9 @@ Bandits.Algorithm ProbabilityTheory.Kernel.traj ProbabilityTheory.Kernel.trajMeasure ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel +Learning.condDistrib_action +Learning.condDistrib_reward +Learning.hasLaw_action_zero Bandits.Algorithm Bandits.Bandit.measure Bandits.arm diff --git a/blueprint/src/chapters/probabilitySpace.tex b/blueprint/src/chapters/probabilitySpace.tex index b6282ee8..8f4dcfbe 100644 --- a/blueprint/src/chapters/probabilitySpace.tex +++ b/blueprint/src/chapters/probabilitySpace.tex @@ -108,12 +108,15 @@ \section{Ionescu-Tulcea theorem} That's the case of an algorithm interacting with an environment as described above. We write $A_t$ and $R_t$ for the projections of $X_t$ on $\mathcal{A}_t$ and $\mathcal{R}_t$ respectively. + \begin{lemma}\label{lem:condDistrib_A_add_one} \uses{def:history, def:trajMeasure} + \leanok + \lean{Learning.condDistrib_action} For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[A_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\pi_t$. \end{lemma} -\begin{proof} +\begin{proof}\leanok \uses{lem:condDistrib_X_add_one} By Lemma~\ref{lem:condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t = \pi_t \otimes \nu_t$. Since $A_{t+1}$ is the projection of $X_{t+1}$ on $\mathcal{A}_{t+1}$, $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}_{t+1}$, which is $\pi_t$. @@ -122,10 +125,12 @@ \section{Ionescu-Tulcea theorem} \begin{lemma}\label{lem:condDistrib_R_add_one} \uses{def:history, def:trajMeasure} + \leanok + \lean{Learning.condDistrib_reward} For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[R_{t+1} \mid H_t, A_{t+1}\right]$ is $((H_t, A_{t+1})_* P_{\mathcal{T}})$-almost surely equal to $\nu_t$. \end{lemma} -\begin{proof} +\begin{proof}\leanok \uses{lem:condDistrib_X_add_one, lem: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:condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t = \pi_t \otimes \nu_t$. @@ -139,10 +144,12 @@ \section{Ionescu-Tulcea theorem} \begin{lemma}\label{lem:law_A_zero} \uses{def:history, def:trajMeasure} + \leanok + \lean{Learning.hasLaw_action_zero} The law of $A_0$ under $P_{\mathcal{T}}$ is $\alpha_0$. \end{lemma} -\begin{proof} +\begin{proof}\leanok \uses{lem:law_X_zero} $X_0$ has law $\mu = \alpha_0 \otimes \nu'_0$. $A_0$ is the projection of $X_0$ on the first space $\mathcal{A}_0$ and $\nu_0'$ is Markov, so $A_0$ has law $\alpha_0$. \end{proof} From f75fe4162f40f50a831d988e50df6dd782186175 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 23 Sep 2025 20:42:19 +0200 Subject: [PATCH 09/17] prove a lemma --- LeanBandits/Algorithm.lean | 8 ++++++++ blueprint/lean_decls | 1 + blueprint/src/chapters/probabilitySpace.tex | 4 +++- 3 files changed, 12 insertions(+), 1 deletion(-) diff --git a/LeanBandits/Algorithm.lean b/LeanBandits/Algorithm.lean index 1daed91d..a80cf454 100644 --- a/LeanBandits/Algorithm.lean +++ b/LeanBandits/Algorithm.lean @@ -187,6 +187,14 @@ lemma hasLaw_action_zero (alg : Algorithm α R) (env : Environment α R) : rw [← fst_comp_step, ← Measure.map_map (by fun_prop) (by fun_prop), (hasLaw_step_zero alg env).map_eq, ← Measure.fst, Measure.fst_compProd] +lemma condDistrib_reward_zero [StandardBorelSpace R] [Nonempty R] + (alg : Algorithm α R) (env : Environment α R) : + condDistrib (reward 0) (action 0) (trajMeasure alg env) + =ᵐ[(trajMeasure alg env).map (action 0)] env.ν0 := by + have h_step := (hasLaw_step_zero alg env).map_eq + have h_action := (hasLaw_action_zero alg env).map_eq + rwa [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop), h_action] + section DetAlgorithm variable {nextaction : (n : ℕ) → (Iic n → α × R) → α} {h_next : ∀ n, Measurable (nextaction n)} diff --git a/blueprint/lean_decls b/blueprint/lean_decls index 883c158e..599e89e0 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -5,6 +5,7 @@ ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel Learning.condDistrib_action Learning.condDistrib_reward Learning.hasLaw_action_zero +Learning.condDistrib_reward_zero Bandits.Algorithm Bandits.Bandit.measure Bandits.arm diff --git a/blueprint/src/chapters/probabilitySpace.tex b/blueprint/src/chapters/probabilitySpace.tex index 8f4dcfbe..c45eb683 100644 --- a/blueprint/src/chapters/probabilitySpace.tex +++ b/blueprint/src/chapters/probabilitySpace.tex @@ -157,10 +157,12 @@ \section{Ionescu-Tulcea theorem} \begin{lemma}\label{lem:condDistrib_R_zero} \uses{def:history, def:trajMeasure} + \leanok + \lean{Learning.condDistrib_reward_zero} The conditional distribution $P_{\mathcal{T}}\left[R_0 \mid A_0\right]$ is $(A_{0*} P_{\mathcal{T}})$-almost surely equal to $\nu'_0$. \end{lemma} -\begin{proof} +\begin{proof}\leanok \uses{lem:law_X_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}}$. From b5eea818b664f6ecd0c239f242ded9b31f00158d Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 23 Sep 2025 21:05:59 +0200 Subject: [PATCH 10/17] partial refactor of bandit code --- LeanBandits/Algorithm.lean | 5 +- LeanBandits/Bandit.lean | 96 +++++++-------------- LeanBandits/ETC.lean | 2 +- LeanBandits/RewardByCountMeasure.lean | 6 +- LeanBandits/UCB.lean | 2 +- blueprint/lean_decls | 4 +- blueprint/src/chapters/bandit.tex | 2 +- blueprint/src/chapters/probabilitySpace.tex | 2 +- 8 files changed, 44 insertions(+), 75 deletions(-) diff --git a/LeanBandits/Algorithm.lean b/LeanBandits/Algorithm.lean index a80cf454..d886459d 100644 --- a/LeanBandits/Algorithm.lean +++ b/LeanBandits/Algorithm.lean @@ -54,7 +54,10 @@ def detAlgorithm (nextaction : (n : ℕ) → (Iic n → α × R) → α) /-- A stationary environment, in which the distribution of the next reward depends only on the last action. -/ -def stationaryEnv (ν : Kernel α R) (n : ℕ) : Kernel ((Iic n → α × R) × α) R := ν.prodMkLeft _ +@[simps] +def stationaryEnv (ν : Kernel α R) [IsMarkovKernel ν] : Environment α R where + feedback _ := ν.prodMkLeft _ + ν0 := ν /-- Kernel describing the distribution of the next action-reward pair given the history up to `n`. -/ diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index 7947f669..4c3f2d17 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne, Paulo Rauber -/ import Mathlib +import LeanBandits.Algorithm import LeanBandits.ForMathlib.CondDistrib import LeanBandits.ForMathlib.KernelCompositionLemmas import LeanBandits.ForMathlib.Traj @@ -12,7 +13,7 @@ import LeanBandits.ForMathlib.Traj # Bandit -/ -open MeasureTheory ProbabilityTheory Filter Real Finset +open MeasureTheory ProbabilityTheory Filter Real Finset Learning open scoped ENNReal NNReal @@ -22,54 +23,24 @@ variable {α R : Type*} {mα : MeasurableSpace α} {mR : MeasurableSpace R} section MeasureSpace -/-- A stochastic, sequential algorithm. -/ -structure Algorithm (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] where - /-- Policy or sampling rule: distribution of the next pull. -/ - policy : (n : ℕ) → Kernel (Iic n → α × R) α - [h_policy : ∀ n, IsMarkovKernel (policy n)] - /-- Distribution of the first pull. -/ - p0 : Measure α - [hp0 : IsProbabilityMeasure p0] - -instance (alg : Algorithm α R) (n : ℕ) : IsMarkovKernel (alg.policy n) := alg.h_policy n -instance (alg : Algorithm α R) : IsProbabilityMeasure alg.p0 := alg.hp0 - -/-- A deterministic algorithm. -/ -noncomputable -def detAlgorithm (nextArm : (n : ℕ) → (Iic n → α × R) → α) (h_next : ∀ n, Measurable (nextArm n)) - (arm0 : α) : - Algorithm α R where - policy n := Kernel.deterministic (nextArm n) (h_next n) - p0 := Measure.dirac arm0 - namespace Bandit /-- Kernel describing the distribution of the next arm-reward pair given the history up to `n`. -/ noncomputable -def stepKernel (alg : Algorithm α R) (ν : Kernel α R) (n : ℕ) : Kernel (Iic n → α × R) (α × R) := - (alg.policy n) ⊗ₖ ν.prodMkLeft (Iic n → α × R) - -instance (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : - IsMarkovKernel (stepKernel alg ν n) := by - rw [stepKernel] - infer_instance +def stepKernel (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : + Kernel (Iic n → α × R) (α × R) := + Learning.stepKernel alg (stationaryEnv ν) n +deriving IsMarkovKernel @[simp] lemma fst_stepKernel (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : (stepKernel alg ν n).fst = alg.policy n := by - rw [stepKernel, Kernel.fst_compProd] + rw [stepKernel, Learning.fst_stepKernel] @[simp] lemma snd_stepKernel (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : (stepKernel alg ν n).snd = ν ∘ₖ alg.policy n := by - rw [stepKernel, Kernel.snd_compProd_prodMkLeft] - -/-- Kernel sending a partial trajectory of the bandit interaction `Iic n → α × ℝ` to a measure -on `ℕ → α × ℝ`, supported on full trajectories that start with the partial one. -/ -noncomputable def traj (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : - Kernel (Iic n → α × R) (ℕ → α × R) := - ProbabilityTheory.Kernel.traj (X := fun _ ↦ α × R) (stepKernel alg ν) n -deriving IsMarkovKernel + rw [stepKernel, Learning.stepKernel, stationaryEnv_feedback, Kernel.snd_compProd_prodMkLeft] /-- Measure on the sequence of arms pulled and rewards observed generated by the bandit. -/ noncomputable @@ -116,26 +87,23 @@ def reward (n : ℕ) (h : ℕ → α × R) : R := (h n).2 def hist (n : ℕ) (h : ℕ → α × R) : Iic n → α × R := fun i ↦ h i @[fun_prop] -lemma measurable_arm (n : ℕ) : Measurable (arm n (α := α) (R := R)) := by unfold arm; fun_prop +lemma measurable_arm (n : ℕ) : Measurable (arm n (α := α) (R := R)) := measurable_action n @[fun_prop] -lemma measurable_arm_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ arm p.1 p.2) := by - refine measurable_from_prod_countable_right fun n ↦ ?_ - simp only - fun_prop +lemma measurable_arm_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ arm p.1 p.2) := + measurable_action_prod @[fun_prop] -lemma measurable_reward (n : ℕ) : Measurable (reward n (α := α) (R := R)) := by - unfold reward; fun_prop +lemma measurable_reward (n : ℕ) : Measurable (reward n (α := α) (R := R)) := + Learning.measurable_reward n @[fun_prop] -lemma measurable_reward_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ reward p.1 p.2) := by - refine measurable_from_prod_countable_right fun n ↦ ?_ - simp only - fun_prop +lemma measurable_reward_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ reward p.1 p.2) := + Learning.measurable_reward_prod @[fun_prop] -lemma measurable_hist (n : ℕ) : Measurable (hist n (α := α) (R := R)) := by unfold hist; fun_prop +lemma measurable_hist (n : ℕ) : Measurable (hist n (α := α) (R := R)) := + Learning.measurable_hist n lemma hist_eq_frestrictLe : hist = Preorder.frestrictLe («π» := fun _ ↦ α × R) := by @@ -151,7 +119,13 @@ lemma condDistrib_arm_reward [StandardBorelSpace α] [Nonempty α] [StandardBore (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : condDistrib (fun h ↦ (arm (n + 1) h, reward (n + 1) h)) (hist n) (Bandit.trajMeasure alg ν) =ᵐ[(Bandit.trajMeasure alg ν).map (hist n)] Bandit.stepKernel alg ν n := - Kernel.condDistrib_trajMeasure_ae_eq_kernel + Learning.condDistrib_step alg (stationaryEnv ν) n + +lemma condDistrib_reward' [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] + (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : + condDistrib (reward (n + 1)) (fun ω ↦ (hist n ω, arm (n + 1) ω)) (Bandit.trajMeasure alg ν) + =ᵐ[(Bandit.trajMeasure alg ν).map (fun ω ↦ (hist n ω, arm (n + 1) ω))] ν.prodMkLeft _ := + Learning.condDistrib_reward alg (stationaryEnv ν) n lemma condDistrib_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : @@ -168,25 +142,17 @@ lemma condDistrib_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpa lemma condDistrib_arm [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : condDistrib (arm (n + 1)) (hist n) (Bandit.trajMeasure alg ν) - =ᵐ[(Bandit.trajMeasure alg ν).map (hist n)] alg.policy n := by - sorry + =ᵐ[(Bandit.trajMeasure alg ν).map (hist n)] alg.policy n := + Learning.condDistrib_action alg (stationaryEnv ν) n -lemma hasLaw_step_zero - (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : - HasLaw (fun h : ℕ → α × R ↦ h 0) (alg.p0 ⊗ₘ ν) (Bandit.trajMeasure alg ν) where - aemeasurable := Measurable.aemeasurable (by fun_prop) - map_eq := by - simp only [Bandit.trajMeasure, Kernel.trajMeasure] - rw [← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc, - Kernel.deterministic_comp_eq_map, Kernel.traj_zero_map_eval_zero, - Measure.deterministic_comp_eq_map, Measure.map_map (by fun_prop) (by fun_prop)] - simp +lemma hasLaw_step_zero (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : + HasLaw (fun h : ℕ → α × R ↦ h 0) (alg.p0 ⊗ₘ ν) (Bandit.trajMeasure alg ν) := + Learning.hasLaw_step_zero alg (stationaryEnv ν) lemma hasLaw_arm_zero [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : - HasLaw (arm 0) alg.p0 (Bandit.trajMeasure alg ν) where - map_eq := by - sorry + HasLaw (arm 0) alg.p0 (Bandit.trajMeasure alg ν) := + Learning.hasLaw_action_zero alg (stationaryEnv ν) /-- The reward at time `n+1` is independent of the history up to time `n` given the arm at `n+1`. -/ lemma condIndepFun_reward_hist_arm [StandardBorelSpace α] [Nonempty α] diff --git a/LeanBandits/ETC.lean b/LeanBandits/ETC.lean index 85e3c12a..52d1c850 100644 --- a/LeanBandits/ETC.lean +++ b/LeanBandits/ETC.lean @@ -11,7 +11,7 @@ import LeanBandits.Regret -/ -open MeasureTheory ProbabilityTheory Finset +open MeasureTheory ProbabilityTheory Finset Learning open scoped ENNReal NNReal namespace Bandits diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index cb581c7b..a03533cd 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -9,7 +9,7 @@ import LeanBandits.Regret /-! # Laws of `stepsUntil` and `rewardByCount` -/ -open MeasureTheory ProbabilityTheory Finset +open MeasureTheory ProbabilityTheory Finset Learning open scoped ENNReal NNReal namespace Bandits @@ -102,7 +102,7 @@ notation "𝓛[" Y " | " X " ← " x "; " μ "]" => Measure.map Y (μ[|X ⁻¹' notation "𝓛[" Y " | " X "; " μ "]" => condDistrib Y X μ omit [DecidableEq α] [MeasurableSingletonClass α] in -lemma condDistrib_reward' [StandardBorelSpace α] [Nonempty α] (n : ℕ) : +lemma condDistrib_reward'' [StandardBorelSpace α] [Nonempty α] (n : ℕ) : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; Bandit.measure alg ν] =ᵐ[(Bandit.measure alg ν).map (fun ω ↦ arm n ω.1)] ν := by let μ := Bandit.measure alg ν @@ -127,7 +127,7 @@ lemma reward_cond_arm [StandardBorelSpace α] [Nonempty α] [Countable α] (a : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; Bandit.measure alg ν] = ν a := by let μ := Bandit.measure alg ν have h_ra : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ] =ᵐ[μ.map (fun ω ↦ arm n ω.1)] ν := - condDistrib_reward' n + condDistrib_reward'' n have h_eq := condDistrib_ae_eq_cond (μ := μ) (X := fun ω ↦ arm n ω.1) (Y := fun ω ↦ reward n ω.1) (by fun_prop) (by fun_prop) rw [Filter.EventuallyEq, ae_iff_of_countable] at h_ra h_eq diff --git a/LeanBandits/UCB.lean b/LeanBandits/UCB.lean index 3ee285ef..b0db6429 100644 --- a/LeanBandits/UCB.lean +++ b/LeanBandits/UCB.lean @@ -11,7 +11,7 @@ import LeanBandits.Regret -/ -open MeasureTheory ProbabilityTheory Filter Real Finset +open MeasureTheory ProbabilityTheory Filter Real Finset Learning open scoped ENNReal NNReal diff --git a/blueprint/lean_decls b/blueprint/lean_decls index 599e89e0..780678f8 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -1,4 +1,4 @@ -Bandits.Algorithm +Learning.Algorithm ProbabilityTheory.Kernel.traj ProbabilityTheory.Kernel.trajMeasure ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel @@ -6,7 +6,7 @@ Learning.condDistrib_action Learning.condDistrib_reward Learning.hasLaw_action_zero Learning.condDistrib_reward_zero -Bandits.Algorithm +Learning.Algorithm Bandits.Bandit.measure Bandits.arm Bandits.reward diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index 41dab130..30acd0d9 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -4,7 +4,7 @@ \section{Algorithm, bandit and probability space} \begin{definition}[Algorithm]\label{def:algorithm} \leanok - \lean{Bandits.Algorithm} + \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 arm to pull at time $t+1$ given the history of previous pulls and observations, diff --git a/blueprint/src/chapters/probabilitySpace.tex b/blueprint/src/chapters/probabilitySpace.tex index c45eb683..0e85c076 100644 --- a/blueprint/src/chapters/probabilitySpace.tex +++ b/blueprint/src/chapters/probabilitySpace.tex @@ -3,7 +3,7 @@ \chapter{Iterative stochastic algorithms} \begin{definition}[Algorithm]\label{def:algorithm'} \leanok - \lean{Bandits.Algorithm} + \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 pulls and observations, From a66e7ade52166e4177c49f2a83af54a488dce3b1 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 23 Sep 2025 21:31:47 +0200 Subject: [PATCH 11/17] prove a lemma --- LeanBandits/ForMathlib/CondDistrib.lean | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean index d38ff220..9746cd7d 100644 --- a/LeanBandits/ForMathlib/CondDistrib.lean +++ b/LeanBandits/ForMathlib/CondDistrib.lean @@ -7,6 +7,7 @@ import Mathlib.Probability.Independence.Basic import Mathlib.Probability.Independence.Conditional import Mathlib.Probability.Kernel.CompProdEqIff import Mathlib.Probability.Kernel.Composition.Lemmas +import LeanBandits.ForMathlib.KernelCompositionParallelComp open MeasureTheory ProbabilityTheory Finset open scoped ENNReal NNReal @@ -404,11 +405,19 @@ lemma condDistrib_comp' (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) condDistrib (f ∘ Y) X μ =ᵐ[μ.map X] (condDistrib Y X μ).map f := by refine condDistrib_ae_eq_of_measure_eq_compProd₀ hX (by fun_prop) _ ?_ calc μ.map (fun x ↦ (X x, (f ∘ Y) x)) - _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ μ.map (fun x ↦ (X x, Y x)) := by - sorry - _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (μ.map X ⊗ₘ condDistrib Y X μ) := by + _ = (μ.map (fun x ↦ (X x, Y x))).map (Prod.map id f) := by + rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)] + rfl + _ = (μ.map X ⊗ₘ condDistrib Y X μ).map (Prod.map id f) := by rw [compProd_map_condDistrib hY] - _ = μ.map X ⊗ₘ (condDistrib Y X μ).map f := sorry + _ = μ.map X ⊗ₘ (condDistrib Y X μ).map f := by + rw [Measure.compProd_eq_comp_prod, ← Measure.deterministic_comp_eq_map (by fun_prop), + Measure.compProd_eq_comp_prod, Measure.comp_assoc] + congr + rw [← Kernel.deterministic_comp_eq_map hf, ← Kernel.parallelComp_comp_copy, + ← Kernel.parallelComp_comp_copy, ← Kernel.parallelComp_id_left_comp_parallelComp, + ← Kernel.deterministic_parallelComp_deterministic (by fun_prop), Kernel.comp_assoc, + ← Kernel.id] lemma condDistrib_comp (hX : AEMeasurable X μ) {f : β → Ω} (hf : Measurable f) : condDistrib (f ∘ X) X μ =ᵐ[μ.map X] Kernel.deterministic f hf := by From 27c820c37e975bc2415faff04138a084d4a7d795 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 23 Sep 2025 21:36:09 +0200 Subject: [PATCH 12/17] lint --- LeanBandits/Bandit.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index 4c3f2d17..85d6d882 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -149,7 +149,7 @@ lemma hasLaw_step_zero (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel HasLaw (fun h : ℕ → α × R ↦ h 0) (alg.p0 ⊗ₘ ν) (Bandit.trajMeasure alg ν) := Learning.hasLaw_step_zero alg (stationaryEnv ν) -lemma hasLaw_arm_zero [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] +lemma hasLaw_arm_zero (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : HasLaw (arm 0) alg.p0 (Bandit.trajMeasure alg ν) := Learning.hasLaw_action_zero alg (stationaryEnv ν) @@ -165,8 +165,7 @@ lemma condIndepFun_reward_hist_arm [StandardBorelSpace α] [Nonempty α] section DetAlgorithm -variable [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] - {nextArm : (n : ℕ) → (Iic n → α × R) → α} {h_next : ∀ n, Measurable (nextArm n)} +variable {nextArm : (n : ℕ) → (Iic n → α × R) → α} {h_next : ∀ n, Measurable (nextArm n)} {arm0 : α} {ν : Kernel α R} [IsMarkovKernel ν] lemma HasLaw_arm_zero_detAlgorithm : @@ -174,7 +173,7 @@ lemma HasLaw_arm_zero_detAlgorithm : (Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν) where map_eq := (hasLaw_arm_zero _ _).map_eq -lemma arm_zero_detAlgorithm : +lemma arm_zero_detAlgorithm [MeasurableSingletonClass α] : arm 0 =ᵐ[Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν] fun _ ↦ arm0 := by have h_eq : ∀ᵐ x ∂((Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν).map (arm 0)), x = arm0 := by @@ -187,7 +186,8 @@ lemma arm_detAlgorithm_ae_eq (n : ℕ) : fun h ↦ nextArm n (fun i ↦ h i) := by sorry -example : ∀ᵐ h ∂(Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν), +example [MeasurableSingletonClass α] : + ∀ᵐ h ∂(Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν), arm 0 h = arm0 ∧ ∀ n, arm (n + 1) h = nextArm n (fun i ↦ h i) := by rw [eventually_and, ae_all_iff] exact ⟨arm_zero_detAlgorithm, arm_detAlgorithm_ae_eq⟩ From 759853976e82fe6756a4ac38cefac58e8c34fa8d Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 24 Sep 2025 09:51:47 +0200 Subject: [PATCH 13/17] prove condDistrib_reward --- LeanBandits/Bandit.lean | 63 ++++++++++++++++++++++++------- blueprint/src/chapters/bandit.tex | 6 +-- 2 files changed, 52 insertions(+), 17 deletions(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index 85d6d882..2563a8fe 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -115,6 +115,14 @@ protected def filtration (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] Filtration ℕ (inferInstance : MeasurableSpace (ℕ → α × R)) := MeasureTheory.Filtration.piLE (X := fun _ ↦ α × R) +lemma hasLaw_step_zero (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : + HasLaw (fun h : ℕ → α × R ↦ h 0) (alg.p0 ⊗ₘ ν) (Bandit.trajMeasure alg ν) := + Learning.hasLaw_step_zero alg (stationaryEnv ν) + +lemma hasLaw_arm_zero (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : + HasLaw (arm 0) alg.p0 (Bandit.trajMeasure alg ν) := + Learning.hasLaw_action_zero alg (stationaryEnv ν) + lemma condDistrib_arm_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : condDistrib (fun h ↦ (arm (n + 1) h, reward (n + 1) h)) (hist n) (Bandit.trajMeasure alg ν) @@ -127,17 +135,48 @@ lemma condDistrib_reward' [StandardBorelSpace α] [Nonempty α] [StandardBorelSp =ᵐ[(Bandit.trajMeasure alg ν).map (fun ω ↦ (hist n ω, arm (n + 1) ω))] ν.prodMkLeft _ := Learning.condDistrib_reward alg (stationaryEnv ν) n +lemma Measure.snd_compProd_prodMkLeft {α β γ : Type*} + {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} + {μ : Measure (α × β)} [SFinite μ] {κ : Kernel β γ} [IsSFiniteKernel κ] : + (μ ⊗ₘ (κ.prodMkLeft α)).snd = κ ∘ₘ μ.snd := by + ext s hs + rw [Measure.snd_apply hs, Measure.compProd_apply (hs.preimage (by fun_prop)), + Measure.bind_apply hs (by fun_prop), Measure.snd, + lintegral_map (κ.measurable_coe hs) (by fun_prop)] + simp only [Kernel.prodMkLeft_apply] + congr + +lemma Measure.snd_prodAssoc_compProd_prodMkLeft {α β γ : Type*} + {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} + {μ : Measure (α × β)} [SFinite μ] {κ : Kernel β γ} [IsSFiniteKernel κ] : + (((μ ⊗ₘ (κ.prodMkLeft α))).map MeasurableEquiv.prodAssoc).snd = μ.snd ⊗ₘ κ := by + ext s hs + rw [Measure.snd_apply hs, Measure.map_apply (by fun_prop) (hs.preimage (by fun_prop)), + Measure.compProd_apply, Measure.compProd_apply hs, Measure.snd, lintegral_map _ (by fun_prop)] + · simp only [Kernel.prodMkLeft_apply] + congr + · exact Kernel.measurable_kernel_prodMk_left hs + · exact hs.preimage (by fun_prop) + lemma condDistrib_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : condDistrib (reward n) (arm n) (Bandit.trajMeasure alg ν) =ᵐ[(Bandit.trajMeasure alg ν).map (arm n)] ν := by cases n with - | zero => sorry + | zero => + rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)] + change (Bandit.trajMeasure alg ν).map (fun h ↦ h 0) + = (Bandit.trajMeasure alg ν).map (arm 0) ⊗ₘ ν + rw [(hasLaw_arm_zero alg ν).map_eq, (hasLaw_step_zero alg ν).map_eq] | succ n => - have h_ar := condDistrib_arm_reward alg ν n - have h_prod := condDistrib_prod_left (X := arm (n + 1)) (Y := reward (n + 1)) - (T := hist n) (μ := Bandit.trajMeasure alg ν) (by fun_prop) (by fun_prop) (by fun_prop) - sorry + have h_eq := condDistrib_reward' alg ν n + rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)] at h_eq ⊢ + have : (Bandit.trajMeasure alg ν).map (arm (n + 1)) + = ((Bandit.trajMeasure alg ν).map (fun x ↦ (hist n x, arm (n + 1) x))).snd := by + rw [Measure.snd_map_prodMk (by fun_prop)] + rw [this, ← Measure.snd_prodAssoc_compProd_prodMkLeft, ← h_eq, + Measure.snd_map_prodMk (by fun_prop), Measure.map_map (by fun_prop) (by fun_prop)] + congr lemma condDistrib_arm [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : @@ -145,15 +184,6 @@ lemma condDistrib_arm [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace =ᵐ[(Bandit.trajMeasure alg ν).map (hist n)] alg.policy n := Learning.condDistrib_action alg (stationaryEnv ν) n -lemma hasLaw_step_zero (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : - HasLaw (fun h : ℕ → α × R ↦ h 0) (alg.p0 ⊗ₘ ν) (Bandit.trajMeasure alg ν) := - Learning.hasLaw_step_zero alg (stationaryEnv ν) - -lemma hasLaw_arm_zero - (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : - HasLaw (arm 0) alg.p0 (Bandit.trajMeasure alg ν) := - Learning.hasLaw_action_zero alg (stationaryEnv ν) - /-- The reward at time `n+1` is independent of the history up to time `n` given the arm at `n+1`. -/ lemma condIndepFun_reward_hist_arm [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] @@ -161,6 +191,11 @@ lemma condIndepFun_reward_hist_arm [StandardBorelSpace α] [Nonempty α] CondIndepFun (MeasurableSpace.comap (arm (n + 1)) inferInstance) (measurable_arm _).comap_le (reward (n + 1)) (hist n) (Bandit.trajMeasure alg ν) := by rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft (by fun_prop) (by fun_prop) (by fun_prop)] + have h_reward' := condDistrib_reward' alg ν n + have h_reward := condDistrib_reward alg ν (n + 1) + -- rw [← Kernel.compProd_eq_iff] at h_reward' h_reward ⊢ + -- rw [compProd_map_condDistrib (by fun_prop)] at h_reward' ⊢ + -- rw [h_reward'] sorry section DetAlgorithm diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index 30acd0d9..293a709a 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -112,7 +112,7 @@ \section{Algorithm, bandit and probability space} The conditional distribution of the reward $X_t$ given the arm $A_t$ in the bandit probability space $(\Omega, \mathbb{P})$ is $\nu(A_t)$. \end{lemma} -\begin{proof} +\begin{proof}\leanok \end{proof} @@ -124,7 +124,7 @@ \section{Algorithm, bandit and probability space} The law of the arm $A_0$ in the bandit probability space $(\Omega, \mathbb{P})$ is $P_0$. \end{lemma} -\begin{proof} +\begin{proof}\leanok \end{proof} @@ -136,7 +136,7 @@ \section{Algorithm, bandit and probability space} The conditional distribution of the arm $A_{t+1}$ given the history $H_t$ in the bandit probability space $(\Omega, \mathbb{P})$ is $\pi_t(H_t)$. \end{lemma} -\begin{proof} +\begin{proof}\leanok \end{proof} From 020a19eb465568509d1e13cae73592f56e06f996 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 24 Sep 2025 14:29:50 +0200 Subject: [PATCH 14/17] sub on kernels --- LeanBandits.lean | 1 + LeanBandits/Bandit.lean | 23 --- LeanBandits/ForMathlib/CondDistrib.lean | 119 ++++++++++++++ LeanBandits/ForMathlib/KernelSub.lean | 205 ++++++++++++++++++++++++ 4 files changed, 325 insertions(+), 23 deletions(-) create mode 100644 LeanBandits/ForMathlib/KernelSub.lean diff --git a/LeanBandits.lean b/LeanBandits.lean index ee04c0d5..a5d8fef3 100644 --- a/LeanBandits.lean +++ b/LeanBandits.lean @@ -5,6 +5,7 @@ import LeanBandits.ETC import LeanBandits.ForMathlib.CondDistrib import LeanBandits.ForMathlib.KernelCompositionLemmas import LeanBandits.ForMathlib.KernelCompositionParallelComp +import LeanBandits.ForMathlib.KernelSub import LeanBandits.ForMathlib.Traj import LeanBandits.Regret import LeanBandits.RewardByCountMeasure diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index 2563a8fe..a73709c9 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -135,29 +135,6 @@ lemma condDistrib_reward' [StandardBorelSpace α] [Nonempty α] [StandardBorelSp =ᵐ[(Bandit.trajMeasure alg ν).map (fun ω ↦ (hist n ω, arm (n + 1) ω))] ν.prodMkLeft _ := Learning.condDistrib_reward alg (stationaryEnv ν) n -lemma Measure.snd_compProd_prodMkLeft {α β γ : Type*} - {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} - {μ : Measure (α × β)} [SFinite μ] {κ : Kernel β γ} [IsSFiniteKernel κ] : - (μ ⊗ₘ (κ.prodMkLeft α)).snd = κ ∘ₘ μ.snd := by - ext s hs - rw [Measure.snd_apply hs, Measure.compProd_apply (hs.preimage (by fun_prop)), - Measure.bind_apply hs (by fun_prop), Measure.snd, - lintegral_map (κ.measurable_coe hs) (by fun_prop)] - simp only [Kernel.prodMkLeft_apply] - congr - -lemma Measure.snd_prodAssoc_compProd_prodMkLeft {α β γ : Type*} - {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} - {μ : Measure (α × β)} [SFinite μ] {κ : Kernel β γ} [IsSFiniteKernel κ] : - (((μ ⊗ₘ (κ.prodMkLeft α))).map MeasurableEquiv.prodAssoc).snd = μ.snd ⊗ₘ κ := by - ext s hs - rw [Measure.snd_apply hs, Measure.map_apply (by fun_prop) (hs.preimage (by fun_prop)), - Measure.compProd_apply, Measure.compProd_apply hs, Measure.snd, lintegral_map _ (by fun_prop)] - · simp only [Kernel.prodMkLeft_apply] - congr - · exact Kernel.measurable_kernel_prodMk_left hs - · exact hs.preimage (by fun_prop) - lemma condDistrib_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : condDistrib (reward n) (arm n) (Bandit.trajMeasure alg ν) diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean index 9746cd7d..79d3358f 100644 --- a/LeanBandits/ForMathlib/CondDistrib.lean +++ b/LeanBandits/ForMathlib/CondDistrib.lean @@ -3,11 +3,13 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne -/ +import Mathlib.MeasureTheory.Measure.ProbabilityMeasure import Mathlib.Probability.Independence.Basic import Mathlib.Probability.Independence.Conditional import Mathlib.Probability.Kernel.CompProdEqIff import Mathlib.Probability.Kernel.Composition.Lemmas import LeanBandits.ForMathlib.KernelCompositionParallelComp +import LeanBandits.ForMathlib.KernelSub open MeasureTheory ProbabilityTheory Finset open scoped ENNReal NNReal @@ -751,6 +753,123 @@ lemma condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft rw [h1, h2] exact ⟨fun h ↦ by rw [h], fun h ↦ by rw [h1_symm, h1, h2_symm, h2, h]⟩ +lemma Measure.snd_compProd_prodMkLeft {α β γ : Type*} + {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} + {μ : Measure (α × β)} [SFinite μ] {κ : Kernel β γ} [IsSFiniteKernel κ] : + (μ ⊗ₘ (κ.prodMkLeft α)).snd = κ ∘ₘ μ.snd := by + ext s hs + rw [Measure.snd_apply hs, Measure.compProd_apply (hs.preimage (by fun_prop)), + Measure.bind_apply hs (by fun_prop), Measure.snd, + lintegral_map (κ.measurable_coe hs) (by fun_prop)] + simp only [Kernel.prodMkLeft_apply] + congr + +lemma Measure.snd_prodAssoc_compProd_prodMkLeft {α β γ : Type*} + {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} + {μ : Measure (α × β)} [SFinite μ] {κ : Kernel β γ} [IsSFiniteKernel κ] : + (((μ ⊗ₘ (κ.prodMkLeft α))).map MeasurableEquiv.prodAssoc).snd = μ.snd ⊗ₘ κ := by + ext s hs + rw [Measure.snd_apply hs, Measure.map_apply (by fun_prop) (hs.preimage (by fun_prop)), + Measure.compProd_apply, Measure.compProd_apply hs, Measure.snd, lintegral_map _ (by fun_prop)] + · simp only [Kernel.prodMkLeft_apply] + congr + · exact Kernel.measurable_kernel_prodMk_left hs + · exact hs.preimage (by fun_prop) + +lemma ProbabilityMeasure.ext_iff_coe {α : Type*} {mα : MeasurableSpace α} + {μ ν : ProbabilityMeasure α} : + μ = ν ↔ (μ : Measure α) = ν := Subtype.ext_iff + +lemma FiniteMeasure.ext_iff_coe {α : Type*} {mα : MeasurableSpace α} {μ ν : FiniteMeasure α} : + μ = ν ↔ (μ : Measure α) = ν := Subtype.ext_iff + +instance : PartialOrder (FiniteMeasure α) := + PartialOrder.lift _ FiniteMeasure.toMeasure_injective + +lemma FiniteMeasure.le_iff_coe {μ ν : FiniteMeasure α} : + μ ≤ ν ↔ (μ : Measure α) ≤ (ν : Measure α) := Iff.rfl + +noncomputable +instance : Sub (FiniteMeasure α) := + ⟨fun μ ν ↦ ⟨μ.toMeasure - ν.toMeasure, inferInstance⟩⟩ + +lemma FiniteMeasure.sub_def (μ ν : FiniteMeasure α) : + μ - ν = ⟨μ.toMeasure - ν.toMeasure, inferInstance⟩ := + rfl + +@[simp, norm_cast] +theorem FiniteMeasure.toMeasure_sub (μ ν : FiniteMeasure α) : ↑(μ - ν) = (↑μ - ↑ν : Measure α) := + rfl + +instance : CanonicallyOrderedAdd (FiniteMeasure α) where + exists_add_of_le {μ ν} hμν := by + refine ⟨ν - μ, ?_⟩ + rw [FiniteMeasure.ext_iff_coe] + simp only [FiniteMeasure.toMeasure_add, FiniteMeasure.toMeasure_sub] + rw [add_comm, Measure.sub_add_cancel_of_le hμν] + le_self_add μ ν := by + simp only [FiniteMeasure.le_iff_coe, FiniteMeasure.toMeasure_add] + exact Measure.le_add_right le_rfl + +instance : OrderedSub (FiniteMeasure α) where + tsub_le_iff_right μ ν ξ := by + simp only [FiniteMeasure.le_iff_coe, FiniteMeasure.toMeasure_sub, FiniteMeasure.toMeasure_add] + exact Measure.sub_le_iff_add + +instance : MeasurableSub₂ (FiniteMeasure α) where + measurable_sub := by + simp only [FiniteMeasure.sub_def] + refine Measurable.subtype_mk ?_ + refine Measure.measurable_of_measurable_coe _ fun s hs ↦ ?_ + sorry + +instance : MeasurableSingletonClass (Measure α) where + measurableSet_singleton μ := sorry + +instance : MeasurableSingletonClass (FiniteMeasure α) := Subtype.instMeasurableSingletonClass + +lemma Kernel.measurableSet_eq (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] : + MeasurableSet {a | κ a = η a} := by + let κ' : α → FiniteMeasure β := fun a ↦ ⟨κ a, inferInstance⟩ + have hκ' : Measurable κ' := Measurable.subtype_mk (by fun_prop) + let η' : α → FiniteMeasure β := fun a ↦ ⟨η a, inferInstance⟩ + have hη' : Measurable η' := Measurable.subtype_mk (by fun_prop) + have h2 : {a | κ a = η a} + = (fun a ↦ (κ' a, η' a)) ⁻¹' + {p : FiniteMeasure β × FiniteMeasure β | p.fst = p.snd} := by + ext + simp [κ', η', FiniteMeasure.ext_iff_coe] + sorry + rw [h2] + refine MeasurableSet.preimage ?_ (by fun_prop) + refine measurableSet_eq_fun' (by fun_prop) (by fun_prop) + +lemma Kernel.prodMkLeft_ae_eq_iff {κ η : Kernel α β} [IsFiniteKernel κ] [IsFiniteKernel η] + {μ : Measure (γ × α)} : + κ.prodMkLeft γ =ᵐ[μ] η.prodMkLeft γ ↔ κ =ᵐ[μ.snd] η := by + rw [Measure.snd, Filter.EventuallyEq, Filter.EventuallyEq, ae_map_iff (by fun_prop)] + · simp + · exact Kernel.measurableSet_eq κ η + +omit [Nonempty Ω'] in +lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft + [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β] + (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) {η : Kernel Ω' Ω} + [IsMarkovKernel η] + (h : condDistrib Y (fun ω ↦ (X ω, Z ω)) μ =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] η.prodMkLeft _) : + Y ⟂ᵢ[Z, hZ; μ] X := by + have hη_eq : condDistrib Y Z μ =ᵐ[μ.map Z] η := by + rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)] at h ⊢ + have h_snd : μ.map Z = (μ.map (fun ω ↦ (X ω, Z ω))).snd := by + rw [Measure.snd_map_prodMk hX] + rw [h_snd, ← Measure.snd_prodAssoc_compProd_prodMkLeft, ← h, + Measure.map_map (by fun_prop) (by fun_prop), Measure.snd_map_prodMk (by fun_prop)] + congr + rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft hX hY hZ] + refine h.trans ?_ + rw [Kernel.prodMkLeft_ae_eq_iff, Measure.snd_map_prodMk (by fun_prop)] + exact hη_eq.symm + end CondDistrib section Cond diff --git a/LeanBandits/ForMathlib/KernelSub.lean b/LeanBandits/ForMathlib/KernelSub.lean new file mode 100644 index 00000000..a1afe096 --- /dev/null +++ b/LeanBandits/ForMathlib/KernelSub.lean @@ -0,0 +1,205 @@ +/- +Copyright (c) 2025 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +import Mathlib.Probability.Kernel.RadonNikodym + +/-! +# Kernels substraction + +-/ + +open MeasureTheory MeasurableSpace +open scoped ENNReal + +namespace MeasureTheory.Measure + +variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν ξ : Measure α} + +lemma sub_le_iff_add_of_le [IsFiniteMeasure ν] (h_le : ν ≤ μ) : μ - ν ≤ ξ ↔ μ ≤ ξ + ν := by + refine ⟨fun h ↦ ?_, Measure.sub_le_of_le_add⟩ + rw [Measure.le_iff] at h ⊢ + intro s hs + specialize h s hs + simp only [Measure.coe_add, Pi.add_apply] + rwa [Measure.sub_apply hs h_le, tsub_le_iff_right] at h + +lemma sub_le_iff_add [IsFiniteMeasure μ] [IsFiniteMeasure ν] : μ - ν ≤ ξ ↔ μ ≤ ξ + ν := by + refine ⟨fun h ↦ ?_, Measure.sub_le_of_le_add⟩ + obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν + suffices μ.restrict s ≤ ξ.restrict s + ν.restrict s + ∧ μ.restrict sᶜ ≤ ξ.restrict sᶜ + ν.restrict sᶜ by + have h_eq_restrict (μ : Measure α) : μ = μ.restrict s + μ.restrict sᶜ := by + rw [Measure.restrict_add_restrict_compl hs.measurableSet] + rw [h_eq_restrict μ, h_eq_restrict ξ, h_eq_restrict ν] + suffices μ.restrict s + μ.restrict sᶜ + ≤ ξ.restrict s + ν.restrict s + (ξ.restrict sᶜ + ν.restrict sᶜ) by + refine this.trans_eq ?_ + abel + gcongr + · exact this.1 + · exact this.2 + constructor + · have h_le := hs.le_on + refine h_le.trans ?_ + exact Measure.le_add_left le_rfl + · have h_le := hs.ge_on_compl + have h' : μ.restrict sᶜ - ν.restrict sᶜ ≤ ξ.restrict sᶜ := by + rw [← Measure.restrict_sub_eq_restrict_sub_restrict hs.measurableSet.compl] + exact Measure.restrict_mono subset_rfl h + exact (Measure.sub_le_iff_add_of_le h_le).mp h' + +lemma add_sub_of_mutuallySingular (h : μ ⟂ₘ ξ) : μ + (ν - ξ) = μ + ν - ξ := by + let s := h.nullSet + have hs : MeasurableSet s := h.measurableSet_nullSet + suffices μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s + ∧ μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ by + calc μ + (ν - ξ) + _ = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ := by + rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs] + _ = μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) := by abel + _ = (μ.restrict s + ν.restrict s - ξ.restrict s) + + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) := by rw [this.1, this.2] + _ = (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ := by + simp [restrict_sub_eq_restrict_sub_restrict hs, + restrict_sub_eq_restrict_sub_restrict hs.compl] + _ = μ + ν - ξ := by rw [restrict_add_restrict_compl hs] + constructor + · rw [h.restrict_nullSet, restrict_sub_eq_restrict_sub_restrict hs] + simp + · rw [restrict_sub_eq_restrict_sub_restrict hs.compl, h.restrict_compl_nullSet] + simp + +lemma withDensity_sub_aux {f g : α → ℝ≥0∞} [IsFiniteMeasure (μ.withDensity g)] + (hg : Measurable g) (hgf : g ≤ᵐ[μ] f) : + (μ.withDensity f - μ.withDensity g) = μ.withDensity (f - g) := by + refine le_antisymm ?_ ?_ + · refine sub_le_of_le_add ?_ + rw [← withDensity_add_right _ hg] + refine withDensity_mono (ae_of_all _ fun x ↦ ?_) + simp only [Pi.add_apply, Pi.sub_apply] + exact le_tsub_add + · rw [sub_def, le_sInf_iff] + intro ξ hξ + simp only [Set.mem_setOf_eq] at hξ + rw [le_iff] at hξ ⊢ + intro s hs + specialize hξ s hs + simp only [coe_add, Pi.add_apply] at hξ + simp_rw [withDensity_apply _ hs] at hξ ⊢ + simp only [Pi.sub_apply] + rw [lintegral_sub hg] + · rwa [tsub_le_iff_right] + · rw [← withDensity_apply _ hs] + simp + · exact ae_restrict_of_ae hgf + +lemma withDensity_sub {f g : α → ℝ≥0∞} [IsFiniteMeasure (μ.withDensity g)] + (hf : Measurable f) (hg : Measurable g) : + (μ.withDensity f - μ.withDensity g) = μ.withDensity (f - g) := by + refine le_antisymm ?_ ?_ + · refine sub_le_of_le_add ?_ + rw [← withDensity_add_right _ hg] + refine withDensity_mono (ae_of_all _ fun x ↦ ?_) + simp only [Pi.add_apply, Pi.sub_apply] + exact le_tsub_add + · let t := {x | f x ≤ g x} + have ht : MeasurableSet t := measurableSet_le hf hg + rw [← restrict_add_restrict_compl (μ := μ.withDensity (f - g)) ht, + ← restrict_add_restrict_compl (μ := μ.withDensity f - μ.withDensity g) ht] + have h_zero : (μ.withDensity (f - g)).restrict t = 0 := by + simp only [restrict_eq_zero] + rw [withDensity_apply _ ht, lintegral_eq_zero_iff (by fun_prop)] + refine ae_restrict_of_forall_mem ht fun x hx ↦ ?_ + simpa [tsub_eq_zero_iff_le] + rw [h_zero, zero_add] + suffices (μ.withDensity (f - g)).restrict tᶜ + ≤ (μ.withDensity f - μ.withDensity g).restrict tᶜ by + refine this.trans ?_ + exact Measure.le_add_left le_rfl + rw [restrict_sub_eq_restrict_sub_restrict ht.compl] + simp_rw [restrict_withDensity ht.compl] + have : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g) := by + rw [← restrict_withDensity ht.compl] + infer_instance + rw [withDensity_sub_aux hg] + refine ae_restrict_of_forall_mem ht.compl fun x hx ↦ ?_ + simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le, t] at hx + exact hx.le + +lemma sub_apply_eq_rnDeriv_add_singularPart [IsFiniteMeasure μ] [IsFiniteMeasure ν] (s : Set α) : + (μ - ν) s = ν.withDensity (fun a ↦ μ.rnDeriv ν a - 1) s + μ.singularPart ν s := by + have hμ : μ = ν.withDensity (fun a ↦ μ.rnDeriv ν a) + μ.singularPart ν := by + rw [rnDeriv_add_singularPart] + have hν : ν = ν.withDensity 1 := by rw [withDensity_one] + conv_lhs => rw [hν, hμ, add_comm _ (μ.singularPart ν)] + rw [← add_sub_of_mutuallySingular] + swap + · simp only [withDensity_one] + exact mutuallySingular_singularPart μ ν + simp only [coe_add, Pi.add_apply] + have : IsFiniteMeasure (ν.withDensity 1) := by simp only [withDensity_one]; infer_instance + rw [add_comm, withDensity_sub (by fun_prop) (by fun_prop)] + congr + +end MeasureTheory.Measure + +namespace ProbabilityTheory.Kernel + +variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + [CountableOrCountablyGenerated α β] {κ η : Kernel α β} + +noncomputable +instance [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] : + Sub (Kernel α β) where + sub κ η := if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η + then + have := h.1 + have := h.2 + η.withDensity (fun a ↦ κ.rnDeriv η a - 1) + κ.singularPart η + else 0 + +lemma sub_def [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] : + κ - η = if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η + then + have := h.1 + have := h.2 + η.withDensity (fun a ↦ κ.rnDeriv η a - 1) + κ.singularPart η + else 0 := + rfl + +@[simp] +lemma sub_of_not_isSFiniteKernel_left [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] + (h : ¬IsSFiniteKernel κ) : κ - η = 0 := by simp [sub_def, h] + +@[simp] +lemma sub_of_not_isSFiniteKernel_right [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] + (h : ¬IsSFiniteKernel η) : κ - η = 0 := by simp [sub_def, h] + +lemma sub_of_isSFiniteKernel [IsSFiniteKernel κ] [IsSFiniteKernel η] + [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] : + κ - η = η.withDensity (fun a ↦ κ.rnDeriv η a - 1) + κ.singularPart η := by + rw [sub_def, dif_pos] + exact ⟨inferInstance, inferInstance⟩ + +-- todo name +lemma sub_apply_eq_rnDeriv_add_singularPart [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] + [IsSFiniteKernel κ] [IsSFiniteKernel η] (a : α) : + (κ - η) a = η.withDensity (fun a ↦ κ.rnDeriv η a - 1) a + κ.singularPart η a := by + rw [sub_of_isSFiniteKernel] + rfl + +lemma sub_apply [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ] + [IsFiniteKernel η] (a : α) : + (κ - η) a = κ a - η a := by + ext s hs + rw [sub_apply_eq_rnDeriv_add_singularPart, Kernel.withDensity_apply _ (by fun_prop), + Kernel.singularPart_eq_singularPart_measure, Measure.sub_apply_eq_rnDeriv_add_singularPart _] + simp only [Measure.coe_add, Pi.add_apply] + congr 2 + refine MeasureTheory.withDensity_congr_ae ?_ + filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb + simp [← hb] + +end ProbabilityTheory.Kernel From 96aba28af84d0f4fc445bc3dc24bedf95f508fd4 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 24 Sep 2025 15:07:42 +0200 Subject: [PATCH 15/17] prove Kernel.measurableSet_eq --- LeanBandits/ForMathlib/CondDistrib.lean | 34 ++------------ LeanBandits/ForMathlib/KernelSub.lean | 60 +++++++++++++++++++++++++ 2 files changed, 64 insertions(+), 30 deletions(-) diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean index 79d3358f..26f7eef7 100644 --- a/LeanBandits/ForMathlib/CondDistrib.lean +++ b/LeanBandits/ForMathlib/CondDistrib.lean @@ -816,40 +816,14 @@ instance : OrderedSub (FiniteMeasure α) where simp only [FiniteMeasure.le_iff_coe, FiniteMeasure.toMeasure_sub, FiniteMeasure.toMeasure_add] exact Measure.sub_le_iff_add -instance : MeasurableSub₂ (FiniteMeasure α) where - measurable_sub := by - simp only [FiniteMeasure.sub_def] - refine Measurable.subtype_mk ?_ - refine Measure.measurable_of_measurable_coe _ fun s hs ↦ ?_ - sorry - -instance : MeasurableSingletonClass (Measure α) where - measurableSet_singleton μ := sorry - -instance : MeasurableSingletonClass (FiniteMeasure α) := Subtype.instMeasurableSingletonClass - -lemma Kernel.measurableSet_eq (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] : - MeasurableSet {a | κ a = η a} := by - let κ' : α → FiniteMeasure β := fun a ↦ ⟨κ a, inferInstance⟩ - have hκ' : Measurable κ' := Measurable.subtype_mk (by fun_prop) - let η' : α → FiniteMeasure β := fun a ↦ ⟨η a, inferInstance⟩ - have hη' : Measurable η' := Measurable.subtype_mk (by fun_prop) - have h2 : {a | κ a = η a} - = (fun a ↦ (κ' a, η' a)) ⁻¹' - {p : FiniteMeasure β × FiniteMeasure β | p.fst = p.snd} := by - ext - simp [κ', η', FiniteMeasure.ext_iff_coe] - sorry - rw [h2] - refine MeasurableSet.preimage ?_ (by fun_prop) - refine measurableSet_eq_fun' (by fun_prop) (by fun_prop) - -lemma Kernel.prodMkLeft_ae_eq_iff {κ η : Kernel α β} [IsFiniteKernel κ] [IsFiniteKernel η] +lemma Kernel.prodMkLeft_ae_eq_iff [MeasurableSpace.CountableOrCountablyGenerated α β] + {κ η : Kernel α β} [IsFiniteKernel κ] [IsFiniteKernel η] {μ : Measure (γ × α)} : κ.prodMkLeft γ =ᵐ[μ] η.prodMkLeft γ ↔ κ =ᵐ[μ.snd] η := by rw [Measure.snd, Filter.EventuallyEq, Filter.EventuallyEq, ae_map_iff (by fun_prop)] · simp - · exact Kernel.measurableSet_eq κ η + · classical + exact Kernel.measurableSet_eq κ η omit [Nonempty Ω'] in lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft diff --git a/LeanBandits/ForMathlib/KernelSub.lean b/LeanBandits/ForMathlib/KernelSub.lean index a1afe096..16e5886d 100644 --- a/LeanBandits/ForMathlib/KernelSub.lean +++ b/LeanBandits/ForMathlib/KernelSub.lean @@ -202,4 +202,64 @@ lemma sub_apply [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] [IsFinit filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb simp [← hb] +omit [CountableOrCountablyGenerated α β] in +lemma le_iff (κ η : Kernel α β) : κ ≤ η ↔ ∀ a, κ a ≤ η a := Iff.rfl + +lemma sub_le_self [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ] + [IsFiniteKernel η] : + κ - η ≤ κ := by + rw [le_iff] + intro a + rw [sub_apply] + exact Measure.sub_le + +instance [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] + [IsFiniteKernel κ] [IsFiniteKernel η] : IsFiniteKernel (κ - η) := + isFiniteKernel_of_le sub_le_self + +lemma sub_apply_eq_zero_iff_le [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] + [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) : (κ - η) a = 0 ↔ κ a ≤ η a := by + simp_rw [sub_apply_eq_rnDeriv_add_singularPart, + add_eq_zero_iff_of_nonneg (Measure.zero_le _) (Measure.zero_le _)] + refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ + · rw [Kernel.withDensity_apply _ (by fun_prop), withDensity_eq_zero_iff (by fun_prop)] at h + rw [singularPart_eq_zero_iff_absolutelyContinuous κ η a] at h + rw [← Measure.rnDeriv_le_one_iff_le h.2] + filter_upwards [h.1, rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb1 hb2 + rw [← hb2] + simp only [Pi.sub_apply, Pi.one_apply, Pi.zero_apply] at hb1 + rwa [tsub_eq_zero_iff_le] at hb1 + · rw [(singularPart_eq_zero_iff_absolutelyContinuous κ η a).mpr + (Measure.absolutelyContinuous_of_le h)] + rw [Kernel.withDensity_apply _ (by fun_prop), withDensity_eq_zero_iff (by fun_prop)] + simp only [and_true] + suffices κ.rnDeriv η a ≤ᵐ[η a] 1 by + filter_upwards [this] with b hb + simpa [tsub_eq_zero_iff_le] using hb + filter_upwards [Measure.rnDeriv_le_one_of_le h, + rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb1 hb2 + rwa [hb2] + +lemma sub_eq_zero_iff_le [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] + [IsFiniteKernel κ] [IsFiniteKernel η] : κ - η = 0 ↔ κ ≤ η := by + simp [Kernel.ext_iff, le_iff, sub_apply_eq_zero_iff_le] + +lemma measurableSet_eq_zero (κ : Kernel α β) [IsFiniteKernel κ] : + MeasurableSet {a | κ a = 0} := by + have h_sing : {a | κ a = 0} = {a | κ a ⟂ₘ κ a} := by ext; simp + rw [h_sing] + exact measurableSet_mutuallySingular κ κ + +lemma measurableSet_eq [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] + (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] : + MeasurableSet {a | κ a = η a} := by + have h_sub : {a | κ a = η a} = {a | (κ - η) a = 0} ∩ {a | (η - κ) a = 0} := by + ext1 a + simp only [Set.mem_setOf_eq, Set.mem_inter_iff, sub_apply_eq_zero_iff_le] + exact ⟨fun h ↦ by simp [h], fun h ↦ le_antisymm h.1 h.2⟩ + rw [h_sub] + refine MeasurableSet.inter ?_ ?_ + · exact measurableSet_eq_zero _ + · exact measurableSet_eq_zero _ + end ProbabilityTheory.Kernel From d812491707530aac1fc39d6e21e1d1c795b7e03c Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 24 Sep 2025 15:10:39 +0200 Subject: [PATCH 16/17] prove condIndepFun_reward_hist_arm --- LeanBandits/Bandit.lean | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index a73709c9..06be7c03 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -166,14 +166,9 @@ lemma condIndepFun_reward_hist_arm [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] {alg : Algorithm α R} {ν : Kernel α R} [IsMarkovKernel ν] (n : ℕ) : CondIndepFun (MeasurableSpace.comap (arm (n + 1)) inferInstance) - (measurable_arm _).comap_le (reward (n + 1)) (hist n) (Bandit.trajMeasure alg ν) := by - rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft (by fun_prop) (by fun_prop) (by fun_prop)] - have h_reward' := condDistrib_reward' alg ν n - have h_reward := condDistrib_reward alg ν (n + 1) - -- rw [← Kernel.compProd_eq_iff] at h_reward' h_reward ⊢ - -- rw [compProd_map_condDistrib (by fun_prop)] at h_reward' ⊢ - -- rw [h_reward'] - sorry + (measurable_arm _).comap_le (reward (n + 1)) (hist n) (Bandit.trajMeasure alg ν) := + condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft + (by fun_prop) (by fun_prop) (by fun_prop) (condDistrib_reward' alg ν n) section DetAlgorithm From b13e27fd0622a8bf609fd3ab5ec3c341fc673497 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 24 Sep 2025 15:27:16 +0200 Subject: [PATCH 17/17] blueprint update --- blueprint/lean_decls | 2 +- .../{probabilitySpace.tex => algorithm.tex} | 22 ++++++++++++++----- blueprint/src/chapters/bandit.tex | 22 +++++++------------ blueprint/src/content.tex | 2 +- 4 files changed, 26 insertions(+), 22 deletions(-) rename blueprint/src/chapters/{probabilitySpace.tex => algorithm.tex} (91%) diff --git a/blueprint/lean_decls b/blueprint/lean_decls index 780678f8..fa693245 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -1,4 +1,5 @@ Learning.Algorithm +Learning.Environment ProbabilityTheory.Kernel.traj ProbabilityTheory.Kernel.trajMeasure ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel @@ -6,7 +7,6 @@ Learning.condDistrib_action Learning.condDistrib_reward Learning.hasLaw_action_zero Learning.condDistrib_reward_zero -Learning.Algorithm Bandits.Bandit.measure Bandits.arm Bandits.reward diff --git a/blueprint/src/chapters/probabilitySpace.tex b/blueprint/src/chapters/algorithm.tex similarity index 91% rename from blueprint/src/chapters/probabilitySpace.tex rename to blueprint/src/chapters/algorithm.tex index 0e85c076..000a5f16 100644 --- a/blueprint/src/chapters/probabilitySpace.tex +++ b/blueprint/src/chapters/algorithm.tex @@ -1,7 +1,7 @@ \chapter{Iterative stochastic algorithms} -\begin{definition}[Algorithm]\label{def:algorithm'} +\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: @@ -13,6 +13,16 @@ \chapter{Iterative stochastic algorithms} 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} + 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}$. @@ -66,7 +76,7 @@ \section{Ionescu-Tulcea theorem} \begin{definition}\label{def:history} - \leanok % no need for a Lean definition + \mathlibok % no need for a Lean definition 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} @@ -110,7 +120,7 @@ \section{Ionescu-Tulcea theorem} \begin{lemma}\label{lem:condDistrib_A_add_one} - \uses{def:history, def:trajMeasure} + \uses{def:history, def:trajMeasure, def:algorithm, def:environment} \leanok \lean{Learning.condDistrib_action} For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[A_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\pi_t$. @@ -124,7 +134,7 @@ \section{Ionescu-Tulcea theorem} \begin{lemma}\label{lem:condDistrib_R_add_one} - \uses{def:history, def:trajMeasure} + \uses{def:history, def:trajMeasure, def:algorithm, def:environment} \leanok \lean{Learning.condDistrib_reward} For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[R_{t+1} \mid H_t, A_{t+1}\right]$ is $((H_t, A_{t+1})_* P_{\mathcal{T}})$-almost surely equal to $\nu_t$. @@ -143,7 +153,7 @@ \section{Ionescu-Tulcea theorem} \begin{lemma}\label{lem:law_A_zero} - \uses{def:history, def:trajMeasure} + \uses{def:history, def:trajMeasure, def:algorithm, def:environment} \leanok \lean{Learning.hasLaw_action_zero} The law of $A_0$ under $P_{\mathcal{T}}$ is $\alpha_0$. @@ -156,7 +166,7 @@ \section{Ionescu-Tulcea theorem} \begin{lemma}\label{lem:condDistrib_R_zero} - \uses{def:history, def:trajMeasure} + \uses{def:history, def:trajMeasure, def:algorithm, def:environment} \leanok \lean{Learning.condDistrib_reward_zero} The conditional distribution $P_{\mathcal{T}}\left[R_0 \mid A_0\right]$ is $(A_{0*} P_{\mathcal{T}})$-almost surely equal to $\nu'_0$. diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index 293a709a..abb30068 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -2,28 +2,18 @@ \chapter{Stochastic multi-armed bandits} \section{Algorithm, bandit and probability space} -\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 arm to pull at time $t+1$ given the history of previous pulls and observations, - \item $P_0 \in \mathcal{P}(\mathcal{A})$, a probability measure that gives the distribution of the first arm to pull. -\end{itemize} -\end{definition} - +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} - \mathlibok + \uses{def:environment} + \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. \end{definition} - -Note: we don't have a Lean definition for a bandit, since it is just a Markov kernel. - 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)$, @@ -47,6 +37,7 @@ \section{Algorithm, bandit and probability space} The reason for adding the extra stream of rewards is explained in Section~\ref{sec:alt_model}. \begin{definition}[Arms, rewards and history]\label{def:armAndReward} + \uses{def:history} \leanok \lean{Bandits.arm, Bandits.reward, Bandits.hist} For $t \in \mathbb{N}$, we denote by $A_t$ the arm pulled at time $t$ and by $X_t$ the reward received at time $t$. @@ -113,6 +104,7 @@ \section{Algorithm, bandit and probability space} \end{lemma} \begin{proof}\leanok + \uses{lem:condDistrib_R_add_one, lem:condDistrib_R_zero} \end{proof} @@ -125,6 +117,7 @@ \section{Algorithm, bandit and probability space} \end{lemma} \begin{proof}\leanok + \uses{lem:law_A_zero} \end{proof} @@ -137,6 +130,7 @@ \section{Algorithm, bandit and probability space} \end{lemma} \begin{proof}\leanok + \uses{lem:condDistrib_A_add_one} \end{proof} diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index 3fc097c5..2c69b421 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -7,7 +7,7 @@ % can start with a \section or \chapter for instance. \input{chapters/intro.tex} -\input{chapters/probabilitySpace.tex} +\input{chapters/algorithm.tex} \input{chapters/bandit.tex} \input{chapters/concentration.tex} \input{chapters/etc.tex}