diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml index 727b79ff..0ca68b36 100644 --- a/.github/workflows/blueprint.yml +++ b/.github/workflows/blueprint.yml @@ -53,7 +53,7 @@ jobs: - name: Build Verso Documentation run: | - ./build_tutorial.sh + ./scripts/build_docs.sh - name: Compile blueprint and documentation uses: leanprover-community/docgen-action@7b5b9a1822650bd45aaeb4182d94bceba2030f89 # 2026-04-14 diff --git a/.gitignore b/.gitignore index ad3d495a..8b05af42 100644 --- a/.gitignore +++ b/.gitignore @@ -41,9 +41,11 @@ blueprint/src/web.pdf ## Website /home_page/ -## Tutorial -/tutorial/.lake/ -/tutorial/_out/ +## Tutorial and docs +/LMLTutorial/.lake/ +/LMLTutorial/_out/ +/LMLDocs/.lake/ +/LMLDocs/_out/ ## Verso Blueprint /verso_blueprint/.lake/ diff --git a/LMLDocs.lean b/LMLDocs.lean new file mode 100644 index 00000000..aab0bd6a --- /dev/null +++ b/LMLDocs.lean @@ -0,0 +1,4 @@ +import LMLDocs.Docs +import LMLDocs.Front +import LMLDocs.Pages.BasicProbability +import LMLDocs.References diff --git a/tutorial/Manual.lean b/LMLDocs/Docs.lean similarity index 85% rename from tutorial/Manual.lean rename to LMLDocs/Docs.lean index 12eef0ac..d16d7601 100644 --- a/tutorial/Manual.lean +++ b/LMLDocs/Docs.lean @@ -1,6 +1,6 @@ import VersoManual -import Manual.Front +import LMLDocs.Front open Verso.Genre.Manual Verso.Output.Html @@ -16,4 +16,4 @@ def config : RenderConfig := { issueLink := some "https://github.com/LeanMachineLearning/LML/issues", } -def main := manualMain (%doc Manual.Front) (config := config) +def main := manualMain (%doc LMLDocs.Front) (config := config) diff --git a/LMLDocs/Front.lean b/LMLDocs/Front.lean new file mode 100644 index 00000000..8c30526c --- /dev/null +++ b/LMLDocs/Front.lean @@ -0,0 +1,23 @@ +import LMLDocs.Pages.BasicProbability +import VersoManual + +set_option linter.style.header false +set_option linter.style.setOption false +set_option linter.hashCommand false +set_option linter.style.longLine false +set_option pp.rawOnError true +set_option verso.code.warnLineLength 100 + +open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External + +#doc (Manual) "Lean Machine Learning" => +%%% +authors := [] +shortTitle := "Lean Machine Learning" +%%% + +These documentation pages are a manual prototype for definition certification pages for the [Lean Machine Learning](https://leanmachinelearning.org) library. + +Some of it should be automatically generated from the code, but for now it is mostly written by hand. + +{include 0 LMLDocs.Pages.BasicProbability} diff --git a/tutorial/Manual/Pages/BasicProbability.lean b/LMLDocs/Pages/BasicProbability.lean similarity index 92% rename from tutorial/Manual/Pages/BasicProbability.lean rename to LMLDocs/Pages/BasicProbability.lean index 5549b6f0..3940b022 100644 --- a/tutorial/Manual/Pages/BasicProbability.lean +++ b/LMLDocs/Pages/BasicProbability.lean @@ -1,32 +1,41 @@ /- - - Created in 2025 by Rémy Degenne +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 VersoManual - -open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External - +import Mathlib.Probability.Distributions.Gaussian.Real +import Mathlib.Probability.Independence.Basic +import Mathlib.Probability.Moments.Basic + +set_option linter.style.header false +set_option linter.style.setOption false +set_option linter.hashCommand false +set_option linter.style.longLine false set_option pp.rawOnError true +set_option verso.code.warnLineLength 100 -set_option verso.exampleProject "../" - -set_option verso.exampleModule "LeanMachineLearning.Tutorial.BasicProbability" +open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External #doc (Manual) "Probability Spaces and Measures" => %%% htmlSplit := .never %%% +```lean -show +open MeasureTheory ProbabilityTheory +open scoped ENNReal NNReal +``` First, in order to work on probability we need a measurable space. We can define a probability measure on such a space as follows. -```anchor One +```lean variable {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P] ``` The class `MeasurableSpace Ω` defines a sigma-algebra on `Ω`. We then introduced a measure `P` on that sigma-algebra and specified that it should be a probability measure. If we want to work on `ℝ` or another well known type the typeclass inference system will find `[MeasurableSpace ℝ]` on its own. We can write simply -```anchor Two +```lean variable {P : Measure ℝ} [IsProbabilityMeasure P] ``` @@ -36,7 +45,7 @@ For example, the variance of a random variable `X` with respect to the measure ` But perhaps we just want a space with a canonical probability measure, which would be the one used without us having to tell Lean explicitly. That can be done with the `MeasureSpace` class. A `MeasureSpace` is a `MeasurableSpace` with a canonical measure called `volume`. The probability library of Mathlib defines a notation `ℙ` for that measure. We still need to tell that we want it to be a probability measure though. -```anchor Three +```lean variable {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)] ``` Remark 1: in the code above we can't write only `[IsProbabilityMeasure ℙ]` because Lean would then not know to which space the default measure `ℙ` refers to. @@ -59,7 +68,7 @@ If we don't need to work with that topology, `{P : Measure Ω} [IsProbabilityMea An event is a measurable set: there is no special event definition in Mathlib. The probability of that event is the measure of the set. A `Measure` can be applied to a set like a function and returns a value in `ENNReal` (denoted by `ℝ≥0∞`, available after `open scoped ENNReal`). -```anchor Four +```lean example (P : Measure ℝ) (s : Set ℝ) : ℝ≥0∞ := P s ``` The probability of the event `s` is thus `P s`. @@ -76,7 +85,7 @@ For many lemmas to apply, the set `s` will need to be a measurable set. The way # Random variables A random variable is a measurable function from a measurable space to another. -```anchor Five +```lean variable {Ω : Type*} [MeasurableSpace Ω] {X : Ω → ℝ} (hX : Measurable X) ``` In that code we defined a random variable `X` from the measurable space `Ω` to `ℝ` (for which the typeclass inference system finds a measurable space instance). The assumption `hX` states that `X` is measurable, which is necessary for most manipulations. @@ -113,7 +122,7 @@ When writing a theorem about probability on finite spaces, it preferable to writ Some results in probability theory require the sigma-algebra to be the Borel sigma-algebra, generated by the open sets. For example, with the Borel sigma-algebra the open sets are measurable and continuous functions are measurable. For that we first need `Ω` to be a topological space and we then need to add a `[BorelSpace Ω]` variable. -```anchor Six +```lean variable {Ω : Type*} [MeasurableSpace Ω] [TopologicalSpace Ω] [BorelSpace Ω] ``` diff --git a/tutorial/Manual/References.lean b/LMLDocs/References.lean similarity index 100% rename from tutorial/Manual/References.lean rename to LMLDocs/References.lean diff --git a/tutorial/static_files/LigaMenlo-Regular.ttf b/LMLDocs/static_files/LigaMenlo-Regular.ttf similarity index 100% rename from tutorial/static_files/LigaMenlo-Regular.ttf rename to LMLDocs/static_files/LigaMenlo-Regular.ttf diff --git a/tutorial/static_files/favicon.svg b/LMLDocs/static_files/favicon.svg similarity index 100% rename from tutorial/static_files/favicon.svg rename to LMLDocs/static_files/favicon.svg diff --git a/tutorial/static_files/scripts.js b/LMLDocs/static_files/scripts.js similarity index 100% rename from tutorial/static_files/scripts.js rename to LMLDocs/static_files/scripts.js diff --git a/tutorial/static_files/style.css b/LMLDocs/static_files/style.css similarity index 100% rename from tutorial/static_files/style.css rename to LMLDocs/static_files/style.css diff --git a/LMLTutorial.lean b/LMLTutorial.lean new file mode 100644 index 00000000..6872a6d1 --- /dev/null +++ b/LMLTutorial.lean @@ -0,0 +1,8 @@ +import LMLTutorial.Front +import LMLTutorial.Pages.BasicProbability +import LMLTutorial.Pages.DefiningAlgorithm +import LMLTutorial.Pages.Installation +import LMLTutorial.Pages.MarkovKernels +import LMLTutorial.Pages.Martingales +import LMLTutorial.References +import LMLTutorial.Tutorial diff --git a/LMLTutorial/Front.lean b/LMLTutorial/Front.lean new file mode 100644 index 00000000..8020ee3e --- /dev/null +++ b/LMLTutorial/Front.lean @@ -0,0 +1,33 @@ +import LMLTutorial.Pages.BasicProbability +import LMLTutorial.Pages.DefiningAlgorithm +import LMLTutorial.Pages.Installation +import LMLTutorial.Pages.MarkovKernels +import LMLTutorial.Pages.Martingales +import VersoManual + +set_option linter.style.header false +set_option linter.style.setOption false +set_option linter.hashCommand false +set_option linter.style.longLine false +set_option pp.rawOnError true +set_option verso.code.warnLineLength 100 + +open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External + +#doc (Manual) "Lean Machine Learning" => +%%% +authors := [] +shortTitle := "Lean Machine Learning" +%%% + +These tutorial pages will guide you through using the [Lean Machine Learning](https://leanmachinelearning.org) library. + +{include 0 LMLTutorial.Pages.Installation} + +{include 0 LMLTutorial.Pages.BasicProbability} + +{include 0 LMLTutorial.Pages.MarkovKernels} + +{include 0 LMLTutorial.Pages.DefiningAlgorithm} + +{include 0 LMLTutorial.Pages.Martingales} diff --git a/LMLTutorial/Pages/BasicProbability.lean b/LMLTutorial/Pages/BasicProbability.lean new file mode 100644 index 00000000..3940b022 --- /dev/null +++ b/LMLTutorial/Pages/BasicProbability.lean @@ -0,0 +1,130 @@ +/- +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 VersoManual +import Mathlib.Probability.Distributions.Gaussian.Real +import Mathlib.Probability.Independence.Basic +import Mathlib.Probability.Moments.Basic + +set_option linter.style.header false +set_option linter.style.setOption false +set_option linter.hashCommand false +set_option linter.style.longLine false +set_option pp.rawOnError true +set_option verso.code.warnLineLength 100 + +open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External + +#doc (Manual) "Probability Spaces and Measures" => +%%% +htmlSplit := .never +%%% + +```lean -show +open MeasureTheory ProbabilityTheory +open scoped ENNReal NNReal +``` + +First, in order to work on probability we need a measurable space. +We can define a probability measure on such a space as follows. +```lean +variable {Ω : Type*} [MeasurableSpace Ω] + {P : Measure Ω} [IsProbabilityMeasure P] +``` +The class `MeasurableSpace Ω` defines a sigma-algebra on `Ω`. We then introduced a measure `P` on that sigma-algebra and specified that it should be a probability measure. +If we want to work on `ℝ` or another well known type the typeclass inference system will find `[MeasurableSpace ℝ]` on its own. We can write simply +```lean +variable {P : Measure ℝ} [IsProbabilityMeasure P] +``` + +With the code above, we can introduce several probability measures on the same space. When using lemmas and definitions about those measures, we will need to specify which measure we are talking about. +For example, the variance of a random variable `X` with respect to the measure `P` will be `variance X P`. + +But perhaps we just want a space with a canonical probability measure, which would be the one used without us having to tell Lean explicitly. +That can be done with the `MeasureSpace` class. A `MeasureSpace` is a `MeasurableSpace` with a canonical measure called `volume`. +The probability library of Mathlib defines a notation `ℙ` for that measure. We still need to tell that we want it to be a probability measure though. +```lean +variable {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)] +``` +Remark 1: in the code above we can't write only `[IsProbabilityMeasure ℙ]` because Lean would then not know to which space the default measure `ℙ` refers to. +That will not be necessary when we use `ℙ` in proofs because the context will be enough to infer `Ω`. + +Remark 2: a lemma written for `P : Measure Ω` in a `MeasurableSpace Ω` will apply for the special measure `ℙ` in a `MeasureSpace Ω`, but the converse is not true. +Mathlib focuses on generality, hence uses the `MeasurableSpace` spelling for its lemmas. In another context, the convenience of `MeasureSpace` may be preferable. + + +Remark 3: `IsProbabilityMeasure` vs `ProbabilityMeasure`. +The examples above used `{P : Measure Ω} [IsProbabilityMeasure P]` to define a probability measure. That's the standard way to do it. +Mathlib also contains a type `ProbabilityMeasure Ω`: the subtype of measures that are probability measures. +The goal of that type is to work on the set of probability measures on `Ω`. +In particular, it comes with a topology, the topology of convergence in distribution (weak convergence of measures). +If we don't need to work with that topology, `{P : Measure Ω} [IsProbabilityMeasure P]` should be preferred. + + +# Probability of events + +An event is a measurable set: there is no special event definition in Mathlib. +The probability of that event is the measure of the set. +A `Measure` can be applied to a set like a function and returns a value in `ENNReal` (denoted by `ℝ≥0∞`, available after `open scoped ENNReal`). +```lean +example (P : Measure ℝ) (s : Set ℝ) : ℝ≥0∞ := P s +``` +The probability of the event `s` is thus `P s`. +The type `ℝ≥0∞` represents the nonnegative reals and infinity: the measure of a set is a nonnegative real number which in general may be infinite. +If `P` is a probability measure, it actually takes only values up to 1. +The tactic `simp` knows that a probability measure is finite and will use the lemmas `measure_ne_top` or `measure_lt_top` to prove that `P s ≠ ∞` or `P s < ∞`. + +The operations on `ℝ≥0∞` are not as nicely behaved as on `ℝ`: `ℝ≥0∞` is not a ring. For example, subtraction truncates to zero. +If one finds that lemma `lemma_name` used to transform an equation does not apply to `ℝ≥0∞`, a good thing to try is to find a lemma named like `ENNReal.lemma_name_of_something` and use that instead (it will typically require that one variable is not infinite). + +For many lemmas to apply, the set `s` will need to be a measurable set. The way to express that is `MeasurableSet s`. + + +# Random variables + +A random variable is a measurable function from a measurable space to another. +```lean +variable {Ω : Type*} [MeasurableSpace Ω] {X : Ω → ℝ} (hX : Measurable X) +``` +In that code we defined a random variable `X` from the measurable space `Ω` to `ℝ` (for which the typeclass inference system finds a measurable space instance). The assumption `hX` states that `X` is measurable, which is necessary for most manipulations. + +If we define a measure `P` on `Ω`, we can talk about the law or distribution of a random variable `X : Ω → E`. +The law of `X` is a measure on `E`, with value `P (X ⁻¹' s)` on any measurable set `s` of `E`. +This is how we define the map of the measure `P` by `X`, `Measure.map X P` or more succinctly `P.map X`. +There is no specific notation for that law. +To say that `X` is Gaussian with mean 0 and variance 1, write `P.map X = gaussianReal 0 1`. + +The expectation of `X` is the integral of that function against the measure `P`, written `∫ ω, X ω ∂P`. +The notation `P[X]` is shorthand for that expectation. In a `MeasureSpace`, we can further use the notation `𝔼[X]`. + +Remark: there are two types of integrals in Mathlib, Bochner integrals and Lebesgue integrals. +The expectation notations stand for the Bochner integral, which is defined for `X : Ω → E` with `E` a normed space over `ℝ` (`[NormedAddCommGroup E] [NormedSpace ℝ E]`). +They don't work for `Y : Ω → ℝ≥0∞` since `ℝ≥0∞` is not a normed space, but those functions can be integrated with the Lebesgue integral: `∫⁻ ω, Y ω ∂P`. +There is no expectation notation for the Lebesgue integral. + +# Discrete probability + +In discrete probability, measurability is not an issue: every set and every function are measurable. +The typeclass `[DiscreteMeasurableSpace Ω]` signals that every set of `Ω` is measurable and the lemma `MeasurableSet.of_discrete` provides a proof of measurability. +To obtain measurability of a function from `Ω`, use `Measurable.of_discrete`. + +Any countable type with measurable singletons is a `DiscreteMeasurableSpace`, for example `ℕ` or `Fin n`. + +A way to define a probability measure on a discrete space `Ω` is to use the type `PMF Ω`, which stands for probability mass function. +`PMF Ω` is the subtype of functions `Ω → ℝ≥0∞` that sum to 1. +One can get a `Measure Ω` from `p : PMF Ω` with `p.toMeasure`. +When writing a theorem about probability on finite spaces, it preferable to write it for a `Measure` in a `DiscreteMeasurableSpace` than for a `PMF` for better integration with the library. + + +# Additional typeclasses on measurable spaces + +Some results in probability theory require the sigma-algebra to be the Borel sigma-algebra, generated by the open sets. For example, with the Borel sigma-algebra the open sets are measurable and continuous functions are measurable. +For that we first need `Ω` to be a topological space and we then need to add a `[BorelSpace Ω]` variable. +```lean +variable {Ω : Type*} [MeasurableSpace Ω] [TopologicalSpace Ω] [BorelSpace Ω] +``` + +For properties related to conditional distributions, it is often convenient or necessary to work in a standard Borel space (a measurable space arising as the Borel sets of some Polish topology). See the `StandardBorelSpace` typeclass. +Note that a countable discrete measurable space is a standard Borel space, so there is no need to worry about that typeclass when doing discrete probability. diff --git a/tutorial/Manual/Pages/DefiningAlgorithm.lean b/LMLTutorial/Pages/DefiningAlgorithm.lean similarity index 60% rename from tutorial/Manual/Pages/DefiningAlgorithm.lean rename to LMLTutorial/Pages/DefiningAlgorithm.lean index 45b657c8..bc9387d4 100644 --- a/tutorial/Manual/Pages/DefiningAlgorithm.lean +++ b/LMLTutorial/Pages/DefiningAlgorithm.lean @@ -1,12 +1,22 @@ +/- +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 VersoManual +import LeanMachineLearning -open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External - +set_option linter.style.header false +set_option linter.style.setOption false +set_option linter.hashCommand false +set_option linter.style.longLine false set_option pp.rawOnError true +set_option verso.code.warnLineLength 100 -set_option verso.exampleProject "../" +set_option verso.docstring.allowMissing true -set_option verso.exampleModule "LeanMachineLearning" +open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External + Learning #doc (Manual) "Defining an Algorithm" => %%% @@ -23,15 +33,7 @@ An algorithm takes actions, to which the environment responds with feedback (e.g In general, both action and feedback can depend on the entire history up to the current time and can be randomized. The `Algorithm` structure is defined as follows: -```anchor Algorithm (module := LeanMachineLearning.SequentialLearning.Algorithm) -structure Algorithm (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where - /-- Policy or sampling rule: distribution of the next action. -/ - policy : (n : ℕ) → Kernel (Iic n → 𝓐 × 𝓨) 𝓐 - [h_policy : ∀ n, IsMarkovKernel (policy n)] - /-- Distribution of the first action. -/ - p0 : Measure 𝓐 - [hp0 : IsProbabilityMeasure p0] -``` +{docstring Algorithm} This structure refers to two types, the type of actions `𝓐` and the type of feedback `𝓨`. Both are measurable spaces, since we consider stochastic algorithms and environments. @@ -45,44 +47,27 @@ The `h_policy` field records that the measure describing the next action is a pr If the algorithms actions are not random, we can use the `detAlgorithm` definition to build an algorithm from the data of a measurable function for the next action and a choice for the first action. -```anchor detAlgorithm (module := LeanMachineLearning.SequentialLearning.Deterministic) -def detAlgorithm (nextA : (n : ℕ) → (Iic n → 𝓐 × 𝓨) → 𝓐) - (h_next : ∀ n, Measurable (nextA n)) (action0 : 𝓐) : - Algorithm 𝓐 𝓨 where - policy n := Kernel.deterministic (nextA n) (h_next n) - p0 := Measure.dirac action0 -``` +{docstring detAlgorithm} + We can see here that we did not need to prove that the kernels are `IsMarkovKernel` and that the distribution of the first action is a probability measure. Lean knows that deterministic kernels are Markov. The `Environment` structure is the mirror of the `Algorithm` structure, with a kernel for the feedback instead of the actions and a kernel for the first feedback instead of the first action. -```anchor Environment (module := LeanMachineLearning.SequentialLearning.Algorithm) -structure Environment (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where - /-- Distribution of the next observation as function of the past history. -/ - feedback : (n : ℕ) → Kernel ((Iic n → 𝓐 × 𝓨) × 𝓐) 𝓨 - [h_feedback : ∀ n, IsMarkovKernel (feedback n)] - /-- Distribution of the first observation given the first action. -/ - ν0 : Kernel 𝓐 𝓨 - [hp0 : IsMarkovKernel ν0] -``` +{docstring Environment} `ν0` gives the distribution of the first feedback given the first action, and `feedback` gives the distribution of the next feedback given the history and the next action. In many applications the feedback depends only on the last action and not on the prior history. We provide an `obliviousEnv` definition that builds an environment for those cases. -```anchor obliviousEnv (module := LeanMachineLearning.SequentialLearning.StationaryEnv) -def obliviousEnv (ν : ℕ → Kernel 𝓐 𝓨) [∀ n, IsMarkovKernel (ν n)] : Environment 𝓐 𝓨 where - feedback n := (ν (n + 1)).prodMkLeft _ - ν0 := ν 0 -``` +{docstring obliviousEnv} + `(ν (n + 1)).prodMkLeft _` is the kernel `ν (n + 1)` seen as a `Kernel ((Iic n → 𝓐 × 𝓨) × 𝓐) 𝓨` by ignoring the history. If furthermore the feedback kernel does not change with time, we can use the `stationaryEnv` definition to build the environment. -```anchor stationaryEnv (module := LeanMachineLearning.SequentialLearning.StationaryEnv) -def stationaryEnv (ν : Kernel 𝓐 𝓨) [IsMarkovKernel ν] : Environment 𝓐 𝓨 := obliviousEnv fun _ ↦ ν -``` + +{docstring stationaryEnv} # Sequences of actions and feedback, probability space @@ -90,20 +75,7 @@ def stationaryEnv (ν : Kernel 𝓐 𝓨) [IsMarkovKernel ν] : Environment 𝓐 Once algorithm and environment are defined, we can introduce sequences of actions and feedback and assume that they are generated by the interaction of the algorithm with the environment. This is done by the `IsAlgEnvSeq` structure. -```anchor IsAlgEnvSeq (module := LeanMachineLearning.SequentialLearning.Algorithm) -structure IsAlgEnvSeq - (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) - (P : Measure Ω) [IsFiniteMeasure P] : Prop where - measurable_action n : Measurable (A n) := by fun_prop - measurable_feedback n : Measurable (Y n) := by fun_prop - hasLaw_action_zero : HasLaw (fun ω ↦ (A 0 ω)) alg.p0 P - hasCondDistrib_feedback_zero : HasCondDistrib (Y 0) (A 0) env.ν0 P - hasCondDistrib_action n : - HasCondDistrib (A (n + 1)) (IsAlgEnvSeq.hist A Y n) (alg.policy n) P - hasCondDistrib_feedback n : - HasCondDistrib (Y (n + 1)) (fun ω ↦ (IsAlgEnvSeq.hist A Y n ω, A (n + 1) ω)) - (env.feedback n) P -``` +{docstring IsAlgEnvSeq} This structure takes as input two sequences of random variables (two stochastic processes), `A` and `Y`, which represent the actions and feedback generated by the interaction of the algorithm with the environment. It states that those sequences are measurable and that they have the correct conditional distributions given by the algorithm and environment. @@ -114,11 +86,8 @@ All spaces of interest in machine learning are standard Borel, so this is not a Given any algorithm and environment, there always exists a sequence of actions and feedback that satisfies `IsAlgEnvSeq` by the Ionescu-Tulcea theorem. However other constructions of such sequences are possible, and it is easier to work with generic sequences satisfying `IsAlgEnvSeq` than with a specific construction. Which sequence we choose does not matter for the results we prove, since all such sequences are equal in distribution, as stated by the following theorem. -```anchor isAlgEnvSeq_unique (module := LeanMachineLearning.SequentialLearning.IonescuTulceaSpace) -theorem isAlgEnvSeq_unique (h1 : IsAlgEnvSeq A₁ R₁ alg env P) - (h2 : IsAlgEnvSeq A₂ R₂ alg env P') : - P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω)) := by -``` + +{docstring isAlgEnvSeq_unique} # Example: the UCB algorithm and a stochastic bandit environment @@ -138,33 +107,14 @@ To define the algorithm, we first define the exploration bonus and the next acti We also need to prove that the next action function is measurable, which is done by the `measurable_nextArm` lemma. Note that we are careful to use a measurable version of the argmax function, `measurableArgmax`. -```anchor UCB_def (module := LeanMachineLearning.Online.Bandit.Algorithms.UCB) -/-- The exploration bonus of the UCB algorithm, which corresponds to the width of -a confidence interval. -/ -noncomputable def ucbWidth' (c : ℝ) (n : ℕ) (h : Iic n → Fin K × ℝ) (a : Fin K) : ℝ := - √(2 * c * log (n + 2) / pullCount' n h a) - -open Classical in -/-- Arm pulled by the UCB algorithm at time `n + 1`. -/ -noncomputable -def UCB.nextArm (hK : 0 < K) (c : ℝ) (n : ℕ) (h : Iic n → Fin K × ℝ) : Fin K := - have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK - if n < K - 1 then RoundRobin.nextAction hK n else - measurableArgmax (fun h a ↦ empMean' n h a + ucbWidth' c n h a) h - -@[fun_prop] -lemma UCB.measurable_nextArm (hK : 0 < K) (c : ℝ) (n : ℕ) : Measurable (nextArm hK c n) := by - refine Measurable.ite (by simp) (by fun_prop) ?_ - have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK - refine measurable_measurableArgmax fun a ↦ ?_ - unfold ucbWidth' - fun_prop - -/-- The UCB algorithm. -/ -noncomputable -def ucbAlgorithm (hK : 0 < K) (c : ℝ) : Algorithm (Fin K) ℝ := - detAlgorithm (UCB.nextArm hK c) (by fun_prop) ⟨0, hK⟩ -``` +{docstring Bandits.ucbWidth'} + +{docstring Bandits.UCB.nextArm} + +{docstring Bandits.UCB.measurable_nextArm} + +{docstring Bandits.ucbAlgorithm} + The last line builds the algorithm using `detAlgorithm` and the function `UCB.nextArm`. Its measurability is proved by the `fun_prop` tactic, which proves measurability of functions by using lemmas tagged with `@[fun_prop]`. The last argument `⟨0, hK⟩` is the first action of the algorithm, which is 0 as an element of `Fin K`. @@ -174,22 +124,14 @@ The last argument `⟨0, hK⟩` is the first action of the algorithm, which is 0 We can now state a theorem about the regret of UCB in a stochastic bandit environment (which we won't prove here). Let's first define the regret, which for stochastic bandits is the difference between the mean rewar that the algorithm would have obtained if it played always the best action, and the sum of mean rewards of the actions played. -```anchor regret (module := LeanMachineLearning.Online.Bandit.Regret) -def regret (ν : Kernel 𝓐 ℝ) (A : ℕ → Ω → 𝓐) (t : ℕ) (ω : Ω) : ℝ := - t * (⨆ a, (ν a)[id]) - ∑ s ∈ range t, (ν (A s ω))[id] -``` +{docstring Bandits.regret} + The quantity `(ν a)[id]` is the mean reward of action `a` in the environment defined by `ν`. We can now state the regret bound for UCB. -```anchor UCB.regret_le (module := LeanMachineLearning.Online.Bandit.Algorithms.UCB) -lemma regret_le [Nonempty (Fin K)] - (h : IsAlgEnvSeq A R (ucbAlgorithm hK (c * σ2)) (stationaryEnv ν) P) - (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) - (hσ2 : σ2 ≠ 0) (hc : 0 < c) (n : ℕ) : - P[regret ν A n] ≤ - ∑ a, (8 * c * σ2 * log (n + 1) / gap ν a + gap ν a * (2 + 2 * (constSum c n).toReal)) := by -``` +{docstring Bandits.UCB.regret_le} + The arguments of the theorem are the following: - `h` states that the sequence of actions and rewards we are considering is generated by the interaction of UCB with parameter `c * σ2` with the stationary environment defined by `ν`. - `hν` states that the reward distribution of each arm is subgaussian with variance proxy `σ2`. @@ -204,15 +146,13 @@ The theorem gives an upper bound on the expected regret of UCB at time `n`. When building an algorithm, we describe it with functions from the history `(Iic n → 𝓐 × R)` to the action space `𝓐`. Thus, to construct UCB, we used the following empirical mean function. -```anchor empMean' (module := LeanMachineLearning.SequentialLearning.FiniteActions) -def empMean' (n : ℕ) (h : Iic n → 𝓐 × ℝ) (a : 𝓐) := - (sumRewards' n h a) / (pullCount' n h a) -``` + +{docstring empMean'} + When analyzing an algorithm, we work with sequences of actions and rewards `A : ℕ → Ω → 𝓐` and `R' : ℕ → Ω → R` that satisfy `IsAlgEnvSeq`. For the analysis, the empirical mean is defined as a stochastic process on the same probability space `Ω`. -```anchor empMean (module := LeanMachineLearning.SequentialLearning.FiniteActions) -def empMean (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ) (ω : Ω) : ℝ := - sumRewards A R' a t ω / pullCount A a t ω -``` + +{docstring empMean} + `empMean A R' a` is a stochastic process with type `ℕ → Ω → ℝ` that gives the empirical mean of action `a` at each time. diff --git a/tutorial/Manual/Pages/Installation.lean b/LMLTutorial/Pages/Installation.lean similarity index 93% rename from tutorial/Manual/Pages/Installation.lean rename to LMLTutorial/Pages/Installation.lean index 5dd09dc9..d4c32409 100644 --- a/tutorial/Manual/Pages/Installation.lean +++ b/LMLTutorial/Pages/Installation.lean @@ -1,3 +1,8 @@ +/- +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 VersoManual open Verso.Genre Manual diff --git a/tutorial/Manual/Pages/MarkovKernels.lean b/LMLTutorial/Pages/MarkovKernels.lean similarity index 87% rename from tutorial/Manual/Pages/MarkovKernels.lean rename to LMLTutorial/Pages/MarkovKernels.lean index a3d75bb1..81ce4031 100644 --- a/tutorial/Manual/Pages/MarkovKernels.lean +++ b/LMLTutorial/Pages/MarkovKernels.lean @@ -1,13 +1,20 @@ -import Manual.References +/- +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 LMLTutorial.References import VersoManual +import Mathlib.Probability.Kernel.Composition.Lemmas -open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External - +set_option linter.style.header false +set_option linter.style.setOption false +set_option linter.hashCommand false +set_option linter.style.longLine false set_option pp.rawOnError true +set_option verso.code.warnLineLength 100 -set_option verso.exampleProject "../" - -set_option verso.exampleModule "LeanMachineLearning.Tutorial.MarkovKernel" +open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External #doc (Manual) "Markov Kernels" => %%% @@ -24,7 +31,17 @@ In probability theory, we need functions to be measurable to be able to work wit A transition kernel from a measurable space `𝓧` to a measurable space `𝓨` is a function `𝓧 → Measure 𝓨` that is measurable. What it means in practice is that each time one wants to work with a function that takes measures as values, the right thing to do is to manipulate it as a kernel. -```anchor Kernel +```lean -show + +open MeasureTheory ProbabilityTheory +open scoped ENNReal + +variable {𝓧 𝓨 : Type*} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} +variable {P : Measure 𝓧} [IsProbabilityMeasure P] + {κ : Kernel 𝓧 𝓨} [IsMarkovKernel κ] +``` + +```lean example (κ : Kernel 𝓧 𝓨) (x : 𝓧) : Measure 𝓨 := κ x example (κ : Kernel 𝓧 𝓨) : Measurable κ := κ.measurable @@ -35,7 +52,7 @@ example (f : 𝓧 → Measure 𝓨) (hf : Measurable f) : Kernel 𝓧 𝓨 := Of course there is a big gap in that explanation: what does it mean for a measure-valued function to be measurable? Such a function is measurable if for every measurable set `B` of `𝓨`, the function `𝓧 → ℝ≥0∞` defined by `fun x ↦ κ x B` is measurable. -```anchor Measurability +```lean example (f : 𝓧 → Measure 𝓨) : Measurable f ↔ ∀ B : Set 𝓨, MeasurableSet B → Measurable (fun x : 𝓧 ↦ f x B) := ⟨fun hf _ hB ↦ (Measure.measurable_coe hB).comp hf, @@ -51,7 +68,7 @@ However, the measurability is important in non-discrete spaces. Kernels are fully specified by their action on measurable functions. That is, if two kernels `κ η : Kernel 𝓧 𝓨` are such that for every measurable function `f : 𝓨 → ℝ≥0∞` and every `x : 𝓧`, `∫ y, f y ∂(κ x) = ∫ y, f y ∂(η x)`, then `κ = η`. -```anchor ExtFun +```lean example (κ η : Kernel 𝓧 𝓨) : κ = η ↔ ∀ x f, Measurable f → ∫⁻ y, f y ∂(κ x) = ∫⁻ y, f y ∂(η x) := Kernel.ext_fun_iff @@ -65,7 +82,7 @@ If the supremum of `κ x univ` over `x : 𝓧` is finite, then `κ` is said to b Finally, Mathlib also contains the class of s-finite kernels, which are kernels that can be expressed as a countable sum of finite kernels. Those three properties are denoted by typeclasses {InlineLean.module}`[IsMarkovKernel κ]`, `[IsFiniteKernel κ]` and `[IsSFiniteKernel κ]` respectively. -```anchor Markov +```lean example (κ : Kernel 𝓧 𝓨) [IsMarkovKernel κ] (x : 𝓧) : κ x Set.univ = 1 := by simp diff --git a/tutorial/Manual/Pages/Martingales.lean b/LMLTutorial/Pages/Martingales.lean similarity index 79% rename from tutorial/Manual/Pages/Martingales.lean rename to LMLTutorial/Pages/Martingales.lean index 2b7407a6..5ad7701c 100644 --- a/tutorial/Manual/Pages/Martingales.lean +++ b/LMLTutorial/Pages/Martingales.lean @@ -1,27 +1,42 @@ /- - - Created in 2025 by Rémy Degenne +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 VersoManual - -open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External - +import Mathlib.Probability.Martingale.Convergence +import Mathlib.Probability.Martingale.OptionalStopping +import Mathlib.Probability.Martingale.OptionalSampling + +set_option linter.style.header false +set_option linter.style.setOption false +set_option linter.hashCommand false +set_option linter.style.longLine false set_option pp.rawOnError true +set_option verso.code.warnLineLength 100 -set_option verso.exampleProject "../" - -set_option verso.exampleModule "LeanMachineLearning.Tutorial.Martingales" +open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External #doc (Manual) "Stochastic Processes and Martingales" => %%% htmlSplit := .never %%% +```lean -show +open Filter +open scoped ENNReal NNReal Topology + +open MeasureTheory ProbabilityTheory Set + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} + {P : Measure Ω} [IsProbabilityMeasure P] +``` + # Stochastic processes, filtrations, and martingales -We define a measure space {anchorTerm Variables}`Ω`, with a probability mesure {anchorTerm Variables}`P : Measure Ω`. +We define a measure space {lean}`Ω`, with a probability mesure {lean}`(P : Measure Ω)`. -```anchor Variables +```lean variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P] ``` @@ -30,14 +45,14 @@ Let then `X` be a stochastic process indexed by `ℕ`: a function `ℕ → Ω Here `E` is a Banach space, a complete normed space (that's what the martingale property needs). We will often need a measurability condition on `X` in lemmas, but we don't add it yet. -```anchor Variables2 +```lean variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mE : MeasurableSpace E} {X : ℕ → Ω → E} ``` A filtration is a monotone family of sub-σ-algebras indexed by `ℕ`. -```anchor Filtration -variable {𝓕 : Filtration ℕ mΩ} +```lean +variable {𝓕 : Filtration ℕ mΩ} {n : ℕ} example : ∀ n, 𝓕 n ≤ mΩ := Filtration.le 𝓕 @@ -45,8 +60,8 @@ example {i j : ℕ} (hij : i ≤ j) : 𝓕 i ≤ 𝓕 j := Filtration.mono 𝓕 ``` If `X` is a martingale, then it is adapted to the filtration, which means that for all `n`, -`X n` is (strongly) measurable with respect to {anchorTerm Filtration}`𝓕 n`. -```anchor Martingale +`X n` is (strongly) measurable with respect to {lean}`𝓕 n`. +```lean example (hX : Martingale X 𝓕 P) : StronglyAdapted 𝓕 X := hX.stronglyAdapted example (hX : Martingale X 𝓕 P) (n : ℕ) : StronglyMeasurable[𝓕 n] (X n) := hX.stronglyAdapted n @@ -69,8 +84,8 @@ example {Y : ℕ → Ω → ℝ} (hX : Submartingale Y 𝓕 P) {i j : ℕ} (hij *Almost everywhere martingale convergence theorem*: An L¹-bounded submartingale converges almost everywhere to a `⨆ n, ℱ n`-measurable function. -```anchor AeTendstoLimitProcess -theorem ae_tendsto_limitProcess {Y : ℕ → Ω → ℝ} (hY : Submartingale Y 𝓕 P) +```lean +example {Y : ℕ → Ω → ℝ} (hY : Submartingale Y 𝓕 P) {R : ℝ≥0} (hbdd : ∀ n, eLpNorm (Y n) 1 P ≤ R) : ∀ᵐ ω ∂P, Tendsto (Y · ω) atTop (𝓝 (𝓕.limitProcess Y P ω)) := by classical @@ -95,10 +110,10 @@ theorem ae_tendsto_limitProcess {Y : ℕ → Ω → ℝ} (hY : Submartingale Y # Stopping times -A stopping time with respect to a filtration indexed by `ℕ` is a random time {anchorTerm Variables3}`τ : Ω → ℕ∞` such that -for all `n`, the set `{ω | τ ω ≤ n}` is measurable with respect to {anchorTerm Filtration}`𝓕 n`. +A stopping time with respect to a filtration indexed by `ℕ` is a random time `τ : Ω → ℕ∞` such that +for all `n`, the set `{ω | τ ω ≤ n}` is measurable with respect to {lean}`𝓕 n`. -```anchor Variables3 +```lean variable {τ : Ω → ℕ∞} (hτ : IsStoppingTime 𝓕 τ) example (i : ℕ) : MeasurableSet[𝓕 i] {ω | τ ω ≤ i} := hτ.measurableSet_le i @@ -107,8 +122,8 @@ example (i : ℕ) : MeasurableSet[𝓕 i] {ω | τ ω ≤ i} := hτ.measurableSe *The optional stopping theorem* (fair game theorem): an adapted integrable process `Y` is a submartingale if and only if for all bounded stopping times `τ` and `π` such that `τ ≤ π`, the stopped value of `Y` at `τ` has expectation smaller than its stopped value at `π`. -```anchor submartingale_iff_expected_stoppedValue_mono -theorem submartingale_iff_expected_stoppedValue_mono' {Y : ℕ → Ω → ℝ} (hadp : StronglyAdapted 𝓕 Y) +```lean +example {Y : ℕ → Ω → ℝ} (hadp : StronglyAdapted 𝓕 Y) (hint : ∀ i, Integrable (Y i) P) : Submartingale Y 𝓕 P ↔ ∀ τ π : Ω → ℕ∞, IsStoppingTime 𝓕 τ → IsStoppingTime 𝓕 π → τ ≤ π → (∃ N : ℕ, ∀ x, π x ≤ N) → P[stoppedValue Y τ] ≤ P[stoppedValue Y π] := diff --git a/LMLTutorial/References.lean b/LMLTutorial/References.lean new file mode 100644 index 00000000..78b8ba8a --- /dev/null +++ b/LMLTutorial/References.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +import VersoManual +open Verso.Genre.Manual + +namespace Docs + +def degenne2025markov : ArXiv where + title := inlines!"Markov kernels in Mathlib's probability library" + authors := #[inlines!"Rémy Degenne"] + year := 2025 + id := "2510.04070" + +end Docs diff --git a/LMLTutorial/Tutorial.lean b/LMLTutorial/Tutorial.lean new file mode 100644 index 00000000..760de515 --- /dev/null +++ b/LMLTutorial/Tutorial.lean @@ -0,0 +1,19 @@ +import VersoManual + +import LMLTutorial.Front + +open Verso.Genre.Manual Verso.Output.Html + +def extraHead : Array Verso.Output.Html := #[ + {{}}, + {{}}, + {{}}, +] + +def config : RenderConfig := { + extraHead := extraHead, + sourceLink := some "https://github.com/LeanMachineLearning/LML", + issueLink := some "https://github.com/LeanMachineLearning/LML/issues", +} + +def main := manualMain (%doc LMLTutorial.Front) (config := config) diff --git a/LMLTutorial/static_files/LigaMenlo-Regular.ttf b/LMLTutorial/static_files/LigaMenlo-Regular.ttf new file mode 100644 index 00000000..b1ca21e2 Binary files /dev/null and b/LMLTutorial/static_files/LigaMenlo-Regular.ttf differ diff --git a/LMLTutorial/static_files/favicon.svg b/LMLTutorial/static_files/favicon.svg new file mode 100644 index 00000000..ea497ae3 --- /dev/null +++ b/LMLTutorial/static_files/favicon.svg @@ -0,0 +1 @@ +RealFaviconGeneratorhttps://realfavicongenerator.net \ No newline at end of file diff --git a/LMLTutorial/static_files/scripts.js b/LMLTutorial/static_files/scripts.js new file mode 100644 index 00000000..64c37a8d --- /dev/null +++ b/LMLTutorial/static_files/scripts.js @@ -0,0 +1,23 @@ +window.addEventListener('load', function () { + document.querySelectorAll('.has-info, .warning').forEach(function (el) { + el.classList.remove('has-info', 'warning'); + + el.querySelectorAll('span.hover-container').forEach(function (hoverSpan) { + hoverSpan.remove(); + }); + }); + + document.querySelectorAll('p').forEach(function (p) { + if (p.querySelector('img')) { + p.setAttribute('align', 'center'); + } + }); + + document.querySelectorAll('a[href]').forEach(function (link) { + const url = new URL(link.href, window.location.href); + if (url.hostname !== window.location.hostname) { + link.setAttribute('target', '_blank'); + link.setAttribute('rel', 'noopener noreferrer'); + } + }); +}); diff --git a/LMLTutorial/static_files/style.css b/LMLTutorial/static_files/style.css new file mode 100644 index 00000000..b329089b --- /dev/null +++ b/LMLTutorial/static_files/style.css @@ -0,0 +1,57 @@ +:root { + --accent: #d65d5d; + --accent-compl: #e8a0a0; + --background: #fef9f9; + --background-lighter: #fefcfc; +} + +@font-face { + font-family: "LigaMenlo"; + src: url("LigaMenlo-Regular.ttf"); +} + +body { + text-align: justify; + background-color: var(--background); +} + +p a:visited, +p a:link { + text-decoration: none; + color: var(--accent); +} + +p a:hover { + text-decoration: underline; +} + +.toc { + background-color: var(--background-lighter); +} + +.keyword { + color: var(--accent) !important; +} + +.hl.lean .token.binding-hl, +.hl.lean .literal.string:hover, +.hl.lean .token.typed:hover { + background-color: var(--accent-compl) !important; + border-radius: 2px !important; +} + +.block { + background-color: var(--background-lighter); + padding: 0.4em; + border: 2px solid black; + border-radius: 0.5em; +} + +.tippy-box[data-theme~='lean'] { + background-color: var(--background-lighter) !important; +} + +code { + font-family: "LigaMenlo"; + font-variant-ligatures: normal; +} diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 0aa85f51..41cbabaf 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -31,6 +31,3 @@ public import LeanMachineLearning.SequentialLearning.EvaluationEnv public import LeanMachineLearning.SequentialLearning.FiniteActions public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace public import LeanMachineLearning.SequentialLearning.StationaryEnv -public import LeanMachineLearning.Tutorial.BasicProbability -public import LeanMachineLearning.Tutorial.MarkovKernel -public import LeanMachineLearning.Tutorial.Martingales diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean index 8d4985c0..231a9f86 100644 --- a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean +++ b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean @@ -26,7 +26,6 @@ variable {K : ℕ} section Algorithm --- ANCHOR: UCB_def /-- The exploration bonus of the UCB algorithm, which corresponds to the width of a confidence interval. -/ noncomputable def ucbWidth' (c : ℝ) (n : ℕ) (h : Iic n → Fin K × ℝ) (a : Fin K) : ℝ := @@ -52,7 +51,6 @@ lemma UCB.measurable_nextArm (hK : 0 < K) (c : ℝ) (n : ℕ) : Measurable (next noncomputable def ucbAlgorithm (hK : 0 < K) (c : ℝ) : Algorithm (Fin K) ℝ := detAlgorithm (UCB.nextArm hK c) (by fun_prop) ⟨0, hK⟩ --- ANCHOR_END: UCB_def end Algorithm namespace UCB @@ -573,14 +571,12 @@ lemma expectation_pullCount_le [Nonempty (Fin K)] ring /-- Regret bound for the UCB algorithm. -/ --- ANCHOR: UCB.regret_le lemma regret_le [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (ucbAlgorithm hK (c * σ2)) (stationaryEnv ν) P) (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 0 < c) (n : ℕ) : P[regret ν A n] ≤ ∑ a, (8 * c * σ2 * log (n + 1) / gap ν a + gap ν a * (2 + 2 * (constSum c n).toReal)) := by --- ANCHOR_END: UCB.regret_le refine (integral_regret_le_of_forall_integral_pullCount_le h (fun a h_gap ↦ expectation_pullCount_le h hν hσ2 hc a (lt_of_le_of_ne' gap_nonneg h_gap) n)).trans_eq ?_ diff --git a/LeanMachineLearning/Online/Bandit/Regret.lean b/LeanMachineLearning/Online/Bandit/Regret.lean index 86f03527..20d68f74 100644 --- a/LeanMachineLearning/Online/Bandit/Regret.lean +++ b/LeanMachineLearning/Online/Bandit/Regret.lean @@ -35,9 +35,7 @@ variable {𝓐 Ω : Type*} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {m /-- Gap of an action `a`: difference between the highest mean of the actions and the mean of `a`. -/ noncomputable --- ANCHOR: gap def gap (ν : Kernel 𝓐 ℝ) (a : 𝓐) : ℝ := (⨆ i, (ν i)[id]) - (ν a)[id] --- ANCHOR_END: gap omit [DecidableEq 𝓐] in lemma gap_nonneg [Finite 𝓐] : 0 ≤ gap ν a := by @@ -46,10 +44,8 @@ lemma gap_nonneg [Finite 𝓐] : 0 ≤ gap ν a := by /-- Regret of a sequence of pulls `k : ℕ → 𝓐` at time `t` for the reward kernel `ν ; Kernel 𝓐 ℝ`. -/ noncomputable --- ANCHOR: regret def regret (ν : Kernel 𝓐 ℝ) (A : ℕ → Ω → 𝓐) (t : ℕ) (ω : Ω) : ℝ := t * (⨆ a, (ν a)[id]) - ∑ s ∈ range t, (ν (A s ω))[id] --- ANCHOR_END: regret omit [DecidableEq 𝓐] in lemma regret_eq_sum_gap : regret ν A t ω = ∑ s ∈ range t, gap ν (A s ω) := by diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean index bdb3c405..68f8c297 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithm.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean @@ -27,10 +27,6 @@ an algorithm interacting with an environment. * `prod_left alg`: an `Algorithm 𝓐 (𝓧 × 𝓨)` obtained from an algorithm `alg : Algorithm 𝓐 𝓨` by ignoring the `𝓧` component of each observation. -## Notes - -The `ANCHOR` comments are used to mark code that appears in the tutorials. - -/ @[expose] public section @@ -44,7 +40,6 @@ namespace Learning variable {𝓐 𝓨 Ω : Type*} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} /-- A stochastic, sequential algorithm. -/ --- ANCHOR: Algorithm structure Algorithm (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where /-- Policy or sampling rule: distribution of the next action. -/ policy : (n : ℕ) → Kernel (Iic n → 𝓐 × 𝓨) 𝓐 @@ -52,7 +47,6 @@ structure Algorithm (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace /-- Distribution of the first action. -/ p0 : Measure 𝓐 [hp0 : IsProbabilityMeasure p0] --- ANCHOR_END: Algorithm instance (alg : Algorithm 𝓐 𝓨) (n : ℕ) : IsMarkovKernel (alg.policy n) := alg.h_policy n instance (alg : Algorithm 𝓐 𝓨) : IsProbabilityMeasure alg.p0 := alg.hp0 @@ -65,7 +59,6 @@ def Algorithm.prodLeft (𝓧 : Type*) [MeasurableSpace 𝓧] (alg : Algorithm p0 := alg.p0 /-- A stochastic environment. -/ --- ANCHOR: Environment structure Environment (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where /-- Distribution of the next observation as function of the past history. -/ feedback : (n : ℕ) → Kernel ((Iic n → 𝓐 × 𝓨) × 𝓐) 𝓨 @@ -73,7 +66,6 @@ structure Environment (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpac /-- Distribution of the first observation given the first action. -/ ν0 : Kernel 𝓐 𝓨 [hp0 : IsMarkovKernel ν0] --- ANCHOR_END: Environment instance (env : Environment 𝓐 𝓨) (n : ℕ) : IsMarkovKernel (env.feedback n) := env.h_feedback n instance (env : Environment 𝓐 𝓨) : IsMarkovKernel env.ν0 := env.hp0 @@ -133,7 +125,6 @@ variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [No /-- An algorithm-environment sequence: a sequence of actions and feedbacks generated by an algorithm interacting with an environment. -/ --- ANCHOR: IsAlgEnvSeq structure IsAlgEnvSeq (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (P : Measure Ω) [IsFiniteMeasure P] : Prop where @@ -146,7 +137,6 @@ structure IsAlgEnvSeq hasCondDistrib_feedback n : HasCondDistrib (Y (n + 1)) (fun ω ↦ (IsAlgEnvSeq.hist A Y n ω, A (n + 1) ω)) (env.feedback n) P --- ANCHOR_END: IsAlgEnvSeq /-- An algorithm-environment sequence: a sequence of actions and feedbacks generated by an algorithm interacting with an environment. -/ diff --git a/LeanMachineLearning/SequentialLearning/Deterministic.lean b/LeanMachineLearning/SequentialLearning/Deterministic.lean index 4411541d..17bd24df 100644 --- a/LeanMachineLearning/SequentialLearning/Deterministic.lean +++ b/LeanMachineLearning/SequentialLearning/Deterministic.lean @@ -37,10 +37,6 @@ measurable functions. according to the measurable function `nextA` (with proof of measurability `h_next`), with initial action `action0`. -## Notes - -The `ANCHOR` comments are used to mark code that appears in the tutorials. - -/ @[expose] public section @@ -205,13 +201,11 @@ variable {nextA : (n : ℕ) → (Iic n → 𝓐 × 𝓨) → 𝓐} {h_next : ∀ /-- A deterministic algorithm, which chooses the action given by the function `nextAction`. -/ @[simps] noncomputable --- ANCHOR: detAlgorithm def detAlgorithm (nextA : (n : ℕ) → (Iic n → 𝓐 × 𝓨) → 𝓐) (h_next : ∀ n, Measurable (nextA n)) (action0 : 𝓐) : Algorithm 𝓐 𝓨 where policy n := Kernel.deterministic (nextA n) (h_next n) p0 := Measure.dirac action0 --- ANCHOR_END: detAlgorithm instance : IsDeterministicAlg (detAlgorithm nextA h_next action0) where exists_action0 := ⟨action0, rfl⟩ diff --git a/LeanMachineLearning/SequentialLearning/FiniteActions.lean b/LeanMachineLearning/SequentialLearning/FiniteActions.lean index 03cb9db6..e6b9fc54 100644 --- a/LeanMachineLearning/SequentialLearning/FiniteActions.lean +++ b/LeanMachineLearning/SequentialLearning/FiniteActions.lean @@ -777,17 +777,13 @@ def sumRewards' (n : ℕ) (h : Iic n → 𝓐 × ℝ) (a : 𝓐) := /-- Empirical mean reward obtained when pulling action `a` up to time `t` (exclusive). -/ noncomputable --- ANCHOR: empMean def empMean (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ) (ω : Ω) : ℝ := sumRewards A R' a t ω / pullCount A a t ω --- ANCHOR_END: empMean /-- Empirical mean of arm `a` at time `n`. -/ noncomputable --- ANCHOR: empMean' def empMean' (n : ℕ) (h : Iic n → 𝓐 × ℝ) (a : 𝓐) := (sumRewards' n h a) / (pullCount' n h a) --- ANCHOR_END: empMean' @[simp] lemma sumRewards_zero {R' : ℕ → Ω → ℝ} : sumRewards A R' a 0 = 0 := by ext; simp [sumRewards] diff --git a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean index e8dd506b..9825e1fa 100644 --- a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean +++ b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean @@ -75,11 +75,9 @@ lemma eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil /-- The law of the sequence of actions and observations generated by an algorithm-environment pair is unique: it does not depend on the probability space used. -/ --- ANCHOR: isAlgEnvSeq_unique theorem isAlgEnvSeq_unique (h1 : IsAlgEnvSeq A₁ R₁ alg env P) (h2 : IsAlgEnvSeq A₂ R₂ alg env P') : P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω)) := by --- ANCHOR_END: isAlgEnvSeq_unique rw [eq_trajMeasure_of_isAlgEnvSeq h1, eq_trajMeasure_of_isAlgEnvSeq h2] /-- The law of the sequence of actions and observations generated by an algorithm-environment pair diff --git a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean index c33fb2f7..048e35bf 100644 --- a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean +++ b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean @@ -131,11 +131,9 @@ end IsObliviousEnv /-- An oblivious environment, in which the distribution of the next feedback depends only on the last action, but in a possibly time-dependent manner. -/ @[simps] --- ANCHOR: obliviousEnv def obliviousEnv (ν : ℕ → Kernel 𝓐 𝓨) [∀ n, IsMarkovKernel (ν n)] : Environment 𝓐 𝓨 where feedback n := (ν (n + 1)).prodMkLeft _ ν0 := ν 0 --- ANCHOR_END: obliviousEnv lemma feedback_obliviousEnv (ν : ℕ → Kernel 𝓐 𝓨) [∀ n, IsMarkovKernel (ν n)] (n : ℕ) : (obliviousEnv ν).feedback n = (ν (n + 1)).prodMkLeft _ := by simp [obliviousEnv] @@ -170,9 +168,7 @@ lemma feedbackCondAction_obliviousEnv (ν : ℕ → Kernel 𝓐 𝓨) [hν : ∀ /-- A stationary environment, in which the distribution of the next feedback depends only on the last action. -/ --- ANCHOR: stationaryEnv def stationaryEnv (ν : Kernel 𝓐 𝓨) [IsMarkovKernel ν] : Environment 𝓐 𝓨 := obliviousEnv fun _ ↦ ν --- ANCHOR_END: stationaryEnv @[simp] lemma feedback_stationaryEnv (ν : Kernel 𝓐 𝓨) [IsMarkovKernel ν] (n : ℕ) : diff --git a/LeanMachineLearning/Tutorial/BasicProbability.lean b/LeanMachineLearning/Tutorial/BasicProbability.lean deleted file mode 100644 index cf08ae41..00000000 --- a/LeanMachineLearning/Tutorial/BasicProbability.lean +++ /dev/null @@ -1,72 +0,0 @@ -/- -Copyright (c) 2026 Rémy Degenne. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne --/ -module - -public import Mathlib.Probability.Distributions.Gaussian.Real -public import Mathlib.Probability.Independence.Basic -public import Mathlib.Probability.Moments.Basic - -/-! # Tutorial source file for basic probability --/ - -@[expose] public section - -open MeasureTheory ProbabilityTheory -open scoped ENNReal NNReal - -noncomputable section - -section --- ANCHOR: One -variable {Ω : Type*} [MeasurableSpace Ω] - {P : Measure Ω} [IsProbabilityMeasure P] --- ANCHOR_END: One -end - -section --- ANCHOR: Two -variable {P : Measure ℝ} [IsProbabilityMeasure P] --- ANCHOR_END: Two -end - -section --- ANCHOR: Three -variable {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)] --- ANCHOR_END: Three -end - -section --- ANCHOR: Four -example (P : Measure ℝ) (s : Set ℝ) : ℝ≥0∞ := P s --- ANCHOR_END: Four -end - -section --- ANCHOR: Five -variable {Ω : Type*} [MeasurableSpace Ω] {X : Ω → ℝ} (hX : Measurable X) --- ANCHOR_END: Five -end - -section --- ANCHOR: Six -variable {Ω : Type*} [MeasurableSpace Ω] [TopologicalSpace Ω] [BorelSpace Ω] --- ANCHOR_END: Six -end - - -section --- ANCHOR: Gaussian -example (μ : ℝ) (v : ℝ≥0) : Measure ℝ := gaussianReal μ v --- ANCHOR_END: Gaussian -end - -section --- ANCHOR: Indep -variable {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} - {X : Ω → ℝ} {Y : Ω → ℕ} (hX : Measurable X) (hY : Measurable Y) - (hXY : IndepFun X Y P) --- ANCHOR_END: Indep -end diff --git a/LeanMachineLearning/Tutorial/MarkovKernel.lean b/LeanMachineLearning/Tutorial/MarkovKernel.lean deleted file mode 100644 index 99161719..00000000 --- a/LeanMachineLearning/Tutorial/MarkovKernel.lean +++ /dev/null @@ -1,58 +0,0 @@ -/- -Copyright (c) 2026 Rémy Degenne. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne --/ -module - -public import Mathlib.Probability.Kernel.Composition.Lemmas -public import Mathlib.Tactic.Recall - -/-! # Tutorial source file for Markov kernels --/ - -@[expose] public section - -open MeasureTheory ProbabilityTheory -open scoped ENNReal - --- ANCHOR: Types -variable {𝓧 𝓨 : Type*} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} --- ANCHOR_END: Types - -variable {P : Measure 𝓧} [IsProbabilityMeasure P] - {κ : Kernel 𝓧 𝓨} [IsMarkovKernel κ] - --- ANCHOR: Kernel -example (κ : Kernel 𝓧 𝓨) (x : 𝓧) : Measure 𝓨 := κ x - -example (κ : Kernel 𝓧 𝓨) : Measurable κ := κ.measurable - -example (f : 𝓧 → Measure 𝓨) (hf : Measurable f) : Kernel 𝓧 𝓨 := ⟨f, hf⟩ --- ANCHOR_END: Kernel - --- ANCHOR: Measurability -example (f : 𝓧 → Measure 𝓨) : - Measurable f ↔ ∀ B : Set 𝓨, MeasurableSet B → Measurable (fun x : 𝓧 ↦ f x B) := - ⟨fun hf _ hB ↦ (Measure.measurable_coe hB).comp hf, - Measure.measurable_of_measurable_coe f⟩ --- ANCHOR_END: Measurability - --- ANCHOR: ExtFun -example (κ η : Kernel 𝓧 𝓨) : - κ = η ↔ ∀ x f, Measurable f → ∫⁻ y, f y ∂(κ x) = ∫⁻ y, f y ∂(η x) := - Kernel.ext_fun_iff --- ANCHOR_END: ExtFun - - --- ANCHOR: Markov -example (κ : Kernel 𝓧 𝓨) [IsMarkovKernel κ] (x : 𝓧) : - κ x Set.univ = 1 := by simp - -example (κ : Kernel 𝓧 𝓨) [IsFiniteKernel κ] : - ∃ C : ℝ≥0∞, C < ∞ ∧ ∀ a, κ a Set.univ ≤ C := - IsFiniteKernel.exists_univ_le - -example (κ : Kernel 𝓧 𝓨) [IsFiniteKernel κ] (x : 𝓧) : - IsFiniteMeasure (κ x) := inferInstance --- ANCHOR_END: Markov diff --git a/LeanMachineLearning/Tutorial/Martingales.lean b/LeanMachineLearning/Tutorial/Martingales.lean deleted file mode 100644 index dd4d4883..00000000 --- a/LeanMachineLearning/Tutorial/Martingales.lean +++ /dev/null @@ -1,146 +0,0 @@ -/- -Copyright (c) 2026 Rémy Degenne. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne --/ -module - -public import Mathlib.Probability.Martingale.Convergence -public import Mathlib.Probability.Martingale.OptionalStopping -public import Mathlib.Probability.Martingale.OptionalSampling - -/-! # Tutorial source file for martingales -/ - -@[expose] public section - -open Filter -open scoped ENNReal NNReal Topology -/- - -# Martingales --/ - -/- We open namespaces. The effect is that after that command, we can call lemmas in those namespaces -without their namespace prefix: for example, we can write `inter_comm` instead of `Set.inter_comm`. -Hover over `open` if you want to learn more. -/ -open MeasureTheory ProbabilityTheory Set - -/- We define a measure space `Ω`: a type with a `MeasurableSpace Ω` variable (a σ-algebra) on which -we also define a mesure `P : Measure Ω`. -We then state that `P` is a probability measure. That is, `P univ = 1`, where `univ : Set Ω` is the -universal set in `Ω` (the set that contains all `x : Ω`). -/ - --- ANCHOR: Variables -variable {Ω : Type*} {mΩ : MeasurableSpace Ω} - {P : Measure Ω} [IsProbabilityMeasure P] --- ANCHOR_END: Variables - -/- One can take the measure of a set `A`. -/ --- ANCHOR: ExProba -example {A : Set Ω} : ℝ≥0∞ := P A --- ANCHOR_END: ExProba - -/- `ℝ≥0∞`, or `ENNReal`, is the type of extended non-negative real numbers, which contain `∞`. -Measures can in general take infinite values, but since our `ℙ` is a probability measure, -it actually takes only values up to 1. -`simp` knows that a probability measure is finite and will use the lemmas `measure_ne_top` -or `measure_lt_top` to prove that `ℙ A ≠ ∞` or `ℙ A < ∞`. -The `finiteness` tactic is specialized in proving that `ℝ≥0∞` expressions are finite. - -Hint: use `#check measure_ne_top` to see what that lemma does. - -The operations on `ℝ≥0∞` are not as nicely behaved as on `ℝ`: `ℝ≥0∞` is not a ring and -subtraction truncates to zero for example. If you find that lemma `lemma_name` used to transform -an equation does not apply to `ℝ≥0∞`, try to find a lemma named something like -`ENNReal.lemma_name_of_something` and use that instead. -/ - -/- A stochastic process indexed by `ℕ`: a function `ℕ → Ω → E`. Here `E` is a Banach space, -a complete normed space (that's what the martingale property needs). -We will often need a measurability condition on `X` in lemmas, but we don't add it yet. -/ - --- ANCHOR: Variables2 -variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] - {mE : MeasurableSpace E} {X : ℕ → Ω → E} --- ANCHOR_END: Variables2 - -/- A filtration: a monotone family of sub-σ-algebras indexed by `ℕ`. -Remember that you can learn about a definition by hovering over it, or by using ctrl-click to go to -its declaration. -/ --- ANCHOR: Filtration -variable {𝓕 : Filtration ℕ mΩ} - -example : ∀ n, 𝓕 n ≤ mΩ := Filtration.le 𝓕 - -example {i j : ℕ} (hij : i ≤ j) : 𝓕 i ≤ 𝓕 j := Filtration.mono 𝓕 hij --- ANCHOR_END: Filtration - -/-- If `X` is a martingale, then it is adapted to the filtration, which means that for all `n`, -`X n` is (strongly) measurable with respect to `𝓕 n`. -/ --- ANCHOR: Martingale -example (hX : Martingale X 𝓕 P) : StronglyAdapted 𝓕 X := hX.stronglyAdapted - -example (hX : Martingale X 𝓕 P) (n : ℕ) : StronglyMeasurable[𝓕 n] (X n) := hX.stronglyAdapted n - -example [BorelSpace E] (hX : Martingale X 𝓕 P) (n : ℕ) : Measurable[𝓕 n] (X n) := - (hX.stronglyAdapted n).measurable - -/-- A martingale satisfies the following equality: for all `i ≤ j`, the conditional expectation of -`X j` with respect to `𝓕 i` is equal to `X i`. -/ -example (hX : Martingale X 𝓕 P) {i j : ℕ} (hij : i ≤ j) : P[X j | 𝓕 i] =ᵐ[P] X i := - hX.condExp_ae_eq hij - -/-- For a submartingale, the conditional expectation of `Y j` with respect to `𝓕 i` is greater than -or equal to `Y i`. -/ -example {Y : ℕ → Ω → ℝ} (hX : Submartingale Y 𝓕 P) {i j : ℕ} (hij : i ≤ j) : - Y i ≤ᵐ[P] P[Y j | 𝓕 i] := - hX.ae_le_condExp hij --- ANCHOR_END: Martingale - -/-- **Almost everywhere martingale convergence theorem**: An L¹-bounded submartingale converges -almost everywhere to a `⨆ n, ℱ n`-measurable function. -/ --- ANCHOR: AeTendstoLimitProcess -theorem ae_tendsto_limitProcess {Y : ℕ → Ω → ℝ} (hY : Submartingale Y 𝓕 P) - {R : ℝ≥0} (hbdd : ∀ n, eLpNorm (Y n) 1 P ≤ R) : - ∀ᵐ ω ∂P, Tendsto (Y · ω) atTop (𝓝 (𝓕.limitProcess Y P ω)) := by - classical - suffices ∃ g, StronglyMeasurable[⨆ n, 𝓕 n] g ∧ ∀ᵐ ω ∂P, Tendsto (Y · ω) atTop (𝓝 (g ω)) by - rw [Filtration.limitProcess, dif_pos this] - exact (Classical.choose_spec this).2 - set g' : Ω → ℝ := fun ω ↦ if h : ∃ c, Tendsto (Y · ω) atTop (𝓝 c) then h.choose else 0 - have hle : ⨆ n, 𝓕 n ≤ mΩ := sSup_le fun m ⟨n, hn⟩ ↦ hn ▸ 𝓕.le _ - have hg' : ∀ᵐ ω ∂P.trim hle, Tendsto (Y · ω) atTop (𝓝 (g' ω)) := by - filter_upwards [hY.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω - simp_rw [g', dif_pos hω] - exact hω.choose_spec - have hg'm : AEStronglyMeasurable[⨆ n, 𝓕 n] g' (P.trim hle) := - (@aemeasurable_of_tendsto_metrizable_ae' _ _ (⨆ n, 𝓕 n) _ _ _ _ _ _ _ - (fun n ↦ ((hY.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩ : 𝓕 n ≤ ⨆ n, 𝓕 n) - le_rfl).aemeasurable) hg').aestronglyMeasurable - obtain ⟨g, hgm, hae⟩ := hg'm - have hg : ∀ᵐ ω ∂P.trim hle, Tendsto (Y · ω) atTop (𝓝 (g ω)) := by - filter_upwards [hae, hg'] with ω hω hg'ω using hω ▸ hg'ω - exact ⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩ --- ANCHOR_END: AeTendstoLimitProcess - -/-! ## Stopping times -/ - -/- A stopping time with respect to a filtration is a random time `τ : Ω → ℕ` such that -for all `n`, the set `{ω | τ ω ≤ n}` is measurable with respect to `𝓕 n`. -/ - --- ANCHOR: Variables3 -variable {τ : Ω → ℕ∞} (hτ : IsStoppingTime 𝓕 τ) - -example (i : ℕ) : MeasurableSet[𝓕 i] {ω | τ ω ≤ i} := hτ.measurableSet_le i --- ANCHOR_END: Variables3 - -/-- **The optional stopping theorem** (fair game theorem): an adapted integrable process `Y` -is a submartingale if and only if for all bounded stopping times `τ` and `π` such that `τ ≤ π`, the -stopped value of `Y` at `τ` has expectation smaller than its stopped value at `π`. -/ --- ANCHOR: submartingale_iff_expected_stoppedValue_mono -theorem submartingale_iff_expected_stoppedValue_mono' {Y : ℕ → Ω → ℝ} (hadp : StronglyAdapted 𝓕 Y) - (hint : ∀ i, Integrable (Y i) P) : - Submartingale Y 𝓕 P ↔ ∀ τ π : Ω → ℕ∞, IsStoppingTime 𝓕 τ → IsStoppingTime 𝓕 π → - τ ≤ π → (∃ N : ℕ, ∀ x, π x ≤ N) → P[stoppedValue Y τ] ≤ P[stoppedValue Y π] := - ⟨fun hf _ _ hτ hπ hle ⟨_, hN⟩ => hf.expected_stoppedValue_mono hτ hπ hle hN, - submartingale_of_expected_stoppedValue_mono hadp hint⟩ --- ANCHOR_END: submartingale_iff_expected_stoppedValue_mono diff --git a/LeanMachineLearning/Tutorial/README.md b/LeanMachineLearning/Tutorial/README.md deleted file mode 100644 index c352eec6..00000000 --- a/LeanMachineLearning/Tutorial/README.md +++ /dev/null @@ -1,5 +0,0 @@ -# Tutorial folder - -The files in this folder are used in the tutorials of the website. -Those tutorials are written in verso, which means that they can import Lean files and show dynamical information about the code, like hover tooltips and type information. -The files in this folder provide the code that is quoted in the tutorials. diff --git a/build_all.sh b/build_all.sh deleted file mode 100755 index c0875e81..00000000 --- a/build_all.sh +++ /dev/null @@ -1,23 +0,0 @@ -set -x -e - -# Build tutorial -cd tutorial -lake build -lake exe manual --output _out/site -mkdir -p _out/site/html-multi/static -cp static_files/* _out/site/html-multi/static -cd .. - -cd verso_blueprint -lake exe cache get -lake build -lake exe blueprint-gen --output _out/site -mkdir -p _out/site/html-multi/static -cp static_files/* _out/site/html-multi/static -cd .. - -# Copy outputs to home_page -mkdir -p home_page/tutorial -cp -r tutorial/_out/site/html-multi/* home_page/tutorial -mkdir -p home_page/verso_blueprint -cp -r verso_blueprint/_out/site/html-multi/* home_page/verso_blueprint diff --git a/build_tutorial.sh b/build_tutorial.sh deleted file mode 100755 index b94ef3a5..00000000 --- a/build_tutorial.sh +++ /dev/null @@ -1,13 +0,0 @@ -set -x -e - -# Build tutorial -cd tutorial -lake build -lake exe manual --output _out/site -mkdir -p _out/site/html-multi/static -cp static_files/* _out/site/html-multi/static -cd .. - -# Copy outputs to home_page -mkdir -p home_page/tutorial -cp -r tutorial/_out/site/html-multi/* home_page/tutorial diff --git a/lake-manifest.json b/lake-manifest.json index b189b757..057ce787 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,34 +1,24 @@ {"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/subverso", + [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, - "scope": "", - "rev": "a86770a5eba721c8554d1d7fce741bc4dde3bb61", - "name": "subverso", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/PatrickMassot/checkdecls.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4", - "name": "checkdecls", + "scope": "leanprover-community", + "rev": "f430c194894355b7685b9985ee461bcd6d1b3bf9", + "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "f430c194894355b7685b9985ee461bcd6d1b3bf9", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", + {"url": "https://github.com/leanprover/verso", "type": "git", "subDir": null, "scope": "", - "rev": "f430c194894355b7685b9985ee461bcd6d1b3bf9", - "name": "mathlib", + "rev": "4c6b02ee232211811f9ad1c148ac336122e256d7", + "name": "verso", "manifestFile": "lake-manifest.json", - "inputRev": "f430c194894355b7685b9985ee461bcd6d1b3bf9", + "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -101,6 +91,36 @@ "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/illuminate", + "type": "git", + "subDir": null, + "scope": "", + "rev": "c7a8de81e102ee2a42a7395f98d1ed12a861a43b", + "name": "illuminate", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a86770a5eba721c8554d1d7fce741bc4dde3bb61", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, diff --git a/lakefile.toml b/lakefile.toml index 43ba5405..5b8e48a9 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -9,19 +9,33 @@ relaxedAutoImplicit = false # Enable all mathlib linters: automatically matches what mathlib uses. weak.linter.mathlibStandardSet = true +[[require]] +name = "verso" +git = "https://github.com/leanprover/verso" +rev = "main" + [[require]] name = "mathlib" -git = "https://github.com/leanprover-community/mathlib4.git" +scope = "leanprover-community" rev = "f430c194894355b7685b9985ee461bcd6d1b3bf9" -[[require]] -name = "checkdecls" -git = "https://github.com/PatrickMassot/checkdecls.git" +[[lean_lib]] +name = "LeanMachineLearning" -[[require]] -name = "subverso" -git = "https://github.com/leanprover/subverso" -rev = "main" +[[lean_lib]] +name = "LMLTutorial" +globs = ["LMLTutorial.*"] [[lean_lib]] -name = "LeanMachineLearning" +name = "LMLDocs" +globs = ["LMLDocs.*"] + +[[lean_exe]] +name = "tutorial" +srcDir = "LMLTutorial/" +root = "Tutorial" + +[[lean_exe]] +name = "docs" +srcDir = "LMLDocs/" +root = "Docs" diff --git a/build_blueprint.sh b/scripts/build_blueprint.sh similarity index 100% rename from build_blueprint.sh rename to scripts/build_blueprint.sh diff --git a/scripts/build_docs.sh b/scripts/build_docs.sh new file mode 100755 index 00000000..3939150e --- /dev/null +++ b/scripts/build_docs.sh @@ -0,0 +1,19 @@ +set -x -e + +lake build + +# Build tutorial +lake exe tutorial --output LMLTutorial/_out/site +mkdir -p LMLTutorial/_out/site/html-multi/static +cp LMLTutorial/static_files/* LMLTutorial/_out/site/html-multi/static + +# Build docs +lake exe docs --output LMLDocs/_out/site +mkdir -p LMLDocs/_out/site/html-multi/static +cp LMLDocs/static_files/* LMLDocs/_out/site/html-multi/static + +# Copy outputs to home_page +mkdir -p home_page/tutorial +cp -r LMLTutorial/_out/site/html-multi/* home_page/tutorial +mkdir -p home_page/defdocs +cp -r LMLDocs/_out/site/html-multi/* home_page/defdocs diff --git a/tutorial/Manual/Front.lean b/tutorial/Manual/Front.lean deleted file mode 100644 index e0d4ccb5..00000000 --- a/tutorial/Manual/Front.lean +++ /dev/null @@ -1,32 +0,0 @@ -import Manual.Pages.BasicProbability -import Manual.Pages.DefiningAlgorithm -import Manual.Pages.Installation -import Manual.Pages.MarkovKernels -import Manual.Pages.Martingales -import VersoManual - -open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External - -set_option pp.rawOnError true - -set_option verso.exampleProject "../" - -set_option verso.exampleModule "LeanMachineLearning" - -#doc (Manual) "Lean Machine Learning" => -%%% -authors := [] -shortTitle := "Lean Machine Learning" -%%% - -These tutorial pages will guide you through using the [Lean Machine Learning](https://leanmachinelearning.org) library. - -{include 0 Manual.Pages.Installation} - -{include 0 Manual.Pages.BasicProbability} - -{include 0 Manual.Pages.MarkovKernels} - -{include 0 Manual.Pages.DefiningAlgorithm} - -{include 0 Manual.Pages.Martingales} diff --git a/tutorial/lake-manifest.json b/tutorial/lake-manifest.json deleted file mode 100644 index b9bfd020..00000000 --- a/tutorial/lake-manifest.json +++ /dev/null @@ -1,56 +0,0 @@ -{"version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/leanprover/verso", - "type": "git", - "subDir": null, - "scope": "", - "rev": "14e7bf2c43076234c4f728d94f8b098dbb36e3cd", - "name": "verso", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/illuminate", - "type": "git", - "subDir": null, - "scope": "", - "rev": "c7a8de81e102ee2a42a7395f98d1ed12a861a43b", - "name": "illuminate", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "", - "rev": "744117af710b1c0400cd297c9ce91f8d0ad3a347", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/subverso", - "type": "git", - "subDir": null, - "scope": "", - "rev": "a86770a5eba721c8554d1d7fce741bc4dde3bb61", - "name": "subverso", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}], - "name": "manual", - "lakeDir": ".lake", - "fixedToolchain": false} diff --git a/tutorial/lakefile.toml b/tutorial/lakefile.toml deleted file mode 100644 index 49a2fa3a..00000000 --- a/tutorial/lakefile.toml +++ /dev/null @@ -1,19 +0,0 @@ -name = "manual" -version = "0.1.0" -keywords = ["math"] - -[leanOptions] -autoImplicit = true - -[[require]] -name = "verso" -git = "https://github.com/leanprover/verso" -rev = "main" - -[[lean_lib]] -name = "Manual" -root = "Manual" - -[[lean_exe]] -name = "manual" -root = "Manual" diff --git a/tutorial/lean-toolchain b/tutorial/lean-toolchain deleted file mode 100644 index 6af09a89..00000000 --- a/tutorial/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:v4.31.0-rc2 \ No newline at end of file diff --git a/verso_blueprint/lake-manifest.json b/verso_blueprint/lake-manifest.json index ee383b1c..640b9b3a 100644 --- a/verso_blueprint/lake-manifest.json +++ b/verso_blueprint/lake-manifest.json @@ -1,4 +1,4 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"type": "path", @@ -12,57 +12,57 @@ "type": "git", "subDir": null, "scope": "", - "rev": "fc90d67b46d75e66611f92f016ad3cc2be0cbb88", + "rev": "11c82ed5b84417b0aecc4a22b89ee536ee832ff4", "name": "VersoBlueprint", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "v4.30.0", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/verso", + {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, - "scope": "", - "rev": "7ae82ac2ae54ae5dcc9948a701669e9b596e5cae", - "name": "verso", + "scope": "leanprover-community", + "rev": "1ccad003f48319848becd773bde09f17729eec3e", + "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", - "inherited": false, + "inputRev": "1ccad003f48319848becd773bde09f17729eec3e", + "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/subverso", + {"url": "https://github.com/leanprover/verso", "type": "git", "subDir": null, "scope": "", - "rev": "52b9dfbd2658408e37ae6e8b72601ddeaaa25a0c", - "name": "subverso", + "rev": "4c6b02ee232211811f9ad1c148ac336122e256d7", + "name": "verso", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/PatrickMassot/checkdecls.git", + {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "scope": "", - "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4", - "name": "checkdecls", + "scope": "leanprover-community", + "rev": "1537e3fc7e680d64e06fe5fb95c4c9edee7941c2", + "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", + {"url": "https://github.com/leanprover/verso-slides.git", "type": "git", "subDir": null, "scope": "", - "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95", - "name": "mathlib", + "rev": "2b5ce1ffa9f22743057068128e20aee96a798976", + "name": "«verso-slides»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", + "inputRev": "2b5ce1ffa9f22743057068128e20aee96a798976", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3", + "rev": "744117af710b1c0400cd297c9ce91f8d0ad3a347", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -82,27 +82,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "48d5698bc464786347c1b0d859b18f938420f060", + "rev": "99c763c8a96d3d44fb4994e96eaa51ca4568449d", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.95", - "inherited": true, - "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7152850e7b216a0d409701617721b6e469d34bf6", + "rev": "7897ea6e5cfc6522d355083bdfa798377ab35e11", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -112,7 +102,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d", + "rev": "94346b7b49c36ae871639d1434232f057c193d60", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -122,22 +112,22 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "756e3321fd3b02a85ffda19fef789916223e578c", + "rev": "5dd219c775e402f818b42cd3997b5cf21017babf", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/leanprover/illuminate", "type": "git", "subDir": null, - "scope": "leanprover", - "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", - "name": "Cli", + "scope": "", + "rev": "c7a8de81e102ee2a42a7395f98d1ed12a861a43b", + "name": "illuminate", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", + "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}, + "configFile": "lakefile.lean"}, {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, @@ -147,6 +137,27 @@ "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}], + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a86770a5eba721c8554d1d7fce741bc4dde3bb61", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "baf3e62fbb3502305076ca077e004aea78157c63", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.31.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}], "name": "LMLBlueprint", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/verso_blueprint/lakefile.lean b/verso_blueprint/lakefile.lean index ea9f057a..c08d41ab 100644 --- a/verso_blueprint/lakefile.lean +++ b/verso_blueprint/lakefile.lean @@ -1,8 +1,7 @@ import Lake open Lake DSL -require verso from git "https://github.com/leanprover/verso"@"v4.29.0" -require VersoBlueprint from git "https://github.com/leanprover/verso-blueprint" +require VersoBlueprint from git "https://github.com/leanprover/verso-blueprint"@"v4.30.0" require LeanMachineLearning from "../" package LMLBlueprint where diff --git a/verso_blueprint/lean-toolchain b/verso_blueprint/lean-toolchain index 14791d72..6af09a89 100644 --- a/verso_blueprint/lean-toolchain +++ b/verso_blueprint/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 +leanprover/lean4:v4.31.0-rc2 \ No newline at end of file