Review of the code

LMLTutorial/Pages/BasicProbability.lean

@@ -98,7 +98,8 @@ If we define a measure `P` on `Ω`, we can talk about the law or distribution of
 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`.
+To say that `X` is Gaussian with mean 0 and variance 1, write `HasLaw X (gaussianReal 0 1) P`.
+`HasLaw X μ P` states that `X` is almost everywhere measurable and that `P.map X = μ`; it is the preferred way to state the law of a random variable.
 
 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]`.
@@ -119,7 +120,7 @@ Any countable type with measurable singletons is a `DiscreteMeasurableSpace`, fo
 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.
+When writing a theorem about probability on finite spaces, it is 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

LMLTutorial/Pages/DefiningAlgorithm.lean

@@ -65,7 +65,7 @@ That kernel is called `Algorithm.policyZero`.
 
 Many settings have no observations at all: the algorithm sees only the past rounds. Those are described by taking `𝓞 = Unit`, and we write `noObs Ω` for the corresponding (constant) observation process.
 
-If the algorithms actions are not random, we can use the `Algorithm.deterministic` definition to build an algorithm from the data of a measurable function for the action at each time, as a function of the history before that time and of the current observation.
+If the algorithm's actions are not random, we can use the `Algorithm.deterministic` definition to build an algorithm from the data of a measurable function for the action at each time, as a function of the history before that time and of the current observation.
 The first action is the value of that function at time `0` on the empty history.
 
 {docstring Algorithm.deterministic}
@@ -91,7 +91,7 @@ If furthermore those sequences do not change with time, we can use the `Environm
 
 {docstring Environment.stationary}
 
-When there is no observation (`𝓞 = Unit`), the feedback depends only on the last action. `Environment.banditSeq` builds such an environment from a sequence of kernels `ν : ℕ → Kernel 𝓐 𝓨`, and `Environment.bandit` from a single kernel `ν : Kernel 𝓐 𝓨` used at every time.
+When there is no observation (`𝓞 = Unit`) and the feedback depends only on the current action (and possibly on the time), we get bandit environments. `Environment.banditSeq` builds such an environment from a sequence of kernels `ν : ℕ → Kernel 𝓐 𝓨`, and `Environment.bandit` from a single kernel `ν : Kernel 𝓐 𝓨` used at every time.
 
 {docstring Environment.bandit}
 
@@ -106,8 +106,10 @@ This is done by the `IsAlgEnvSeq` structure.
 This structure takes as input three sequences of random variables (three stochastic processes), `O`, `A` and `Y`, which represent the observations, 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.
 The measurable space `Ω` and the measure `P` are not imposed: they can be chosen as we want, as long as the conditions of `IsAlgEnvSeq` are satisfied.
-This definition requires `𝓐` and `𝓨` to be nonempty standard Borel spaces, because Mathlib's theory about conditional distributions requires those assumptions.
-All spaces of interest in machine learning are standard Borel, so this is not a restriction.
+The conditional distributions are expressed with `HasCondDistrib`: `HasCondDistrib Y X κ P` states that the joint law of `(X, Y)` under `P` is the law of `X` composed with the kernel `κ`.
+This definition makes no assumption on the measurable spaces.
+Some results about algorithm-environment sequences, for example those using Mathlib's conditional distribution `condDistrib` or conditional independence, require the spaces to be nonempty standard Borel spaces.
+All spaces of interest in machine learning are standard Borel, so this is not a restriction in practice.
 
 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.
@@ -148,7 +150,7 @@ The first action of the algorithm is `UCB.nextArm K c 0` applied to the empty hi
 ## A theorem about UCB
 
 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.
+Let's first define the regret, which for stochastic bandits is the difference between the sum of the mean rewards that the algorithm would have obtained if it had always played the best action, and the sum of the mean rewards of the actions played.
 
 {docstring Bandits.regret}
 
@@ -161,7 +163,7 @@ We can now state the regret bound for UCB.
 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`.
-- `hσ2` and `hc` state that the parameters `σ2` and `c` are positive.
+- `hσ2` and `hc` state that the parameters `σ2` and `c` are positive (`σ2` is a nonnegative real number, so `σ2 ≠ 0` means that it is positive).
 - `n` is the time horizon.
 
 The theorem gives an upper bound on the expected regret of UCB at time `n`.
@@ -170,15 +172,16 @@ The theorem gives an upper bound on the expected regret of UCB at time `n`.
 
 # Building vs analyzing algorithms
 
-When building an algorithm, we describe it with functions from the history and the current observation `(Hist 𝓞 𝓐 R n × 𝓞)` to the action space `𝓐`.
+When building an algorithm, we describe it with functions from the history and the current observation `(Hist 𝓞 𝓐 𝓨 n × 𝓞)` to the action space `𝓐`.
 Thus, to construct UCB, we used the following empirical mean function.
 
 {docstring empMean'}
 
 
-When analyzing an algorithm, we work with sequences of actions and rewards `A : ℕ → Ω → 𝓐` and `R' : ℕ → Ω → R` that satisfy `IsAlgEnvSeq`.
+When analyzing an algorithm, we work with sequences of actions and rewards `A : ℕ → Ω → 𝓐` and `R : ℕ → Ω → ℝ` that satisfy `IsAlgEnvSeq`.
 For the analysis, the empirical mean is defined as a stochastic process on the same probability space `Ω`.
 
 {docstring empMean}
 
-`empMean A R' a` is a stochastic process with type `ℕ → Ω → ℝ` that gives the empirical mean of action `a` at each time.
+`empMean A R a` is a stochastic process with type `ℕ → Ω → ℝ` that gives the empirical mean of action `a` at each time.
+The two definitions agree along any sequence: `empMean A R a n ω = empMean' n (history O A R n ω) a` (lemma `empMean_eq_empMean'`), which is how properties of the algorithm, stated with `empMean'`, are transferred to the analysis, stated with `empMean`.

LMLTutorial/Pages/Installation.lean

@@ -60,6 +60,14 @@ name = "LeanMachineLearning"
 git = "https://github.com/LeanMachineLearning/LML"
 ```
 
+Your project must use the same version of Lean as the library: copy the `lean-toolchain` file of the library into your project.
+Then run
+```
+lake update LeanMachineLearning
+lake exe cache get
+```
+to download the library and its dependencies, and to get the precompiled Mathlib cache.
+
 # Testing the installation
 
 Create a new Lean file in your project and add the following code:

LMLTutorial/Pages/MarkovKernels.lean

@@ -72,7 +72,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 `κ = η`.
+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 `κ = η`.
 ```lean
 example (κ η : Kernel 𝓧 𝓨) :
     κ = η ↔ ∀ x f, Measurable f → ∫⁻ y, f y ∂(κ x) = ∫⁻ y, f y ∂(η x) :=
@@ -82,7 +82,7 @@ Another way to show that two kernels are equal is to show that their values `κ
 
 # Classes of kernels
 
-A kernel `κ : 𝓧 ⟶ 𝓨` is a Markov kernel if `κ x` is a probability measure for every `x : 𝓧`.
+A kernel `κ : Kernel 𝓧 𝓨` is a Markov kernel if `κ x` is a probability measure for every `x : 𝓧`.
 If the supremum of `κ x univ` over `x : 𝓧` is finite, then `κ` is said to be a finite kernel.
 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.
@@ -106,7 +106,7 @@ Among the deterministic kernels, a few play a special role.
 The identity kernel `Kernel.id : Kernel 𝓧 𝓧` is the deterministic kernel associated with the identity function: it maps `x` to the Dirac measure at `x`.
 The copy kernel `Kernel.copy : Kernel 𝓧 (𝓧 × 𝓧)` maps `x` to the Dirac measure at `(x, x)`.
 The discard kernel `Kernel.discard : Kernel 𝓧 Unit` maps `x` to the unique probability measure on the one-point space `Unit`.
-Another useful (not deterministic) kernel is the constant kernel `Kernel.const μ : Kernel Ω 𝓧` which maps every point of `Ω` to the same probability measure `μ` on `𝓧`.
+Another useful (not deterministic) kernel is the constant kernel `Kernel.const Ω μ : Kernel Ω 𝓧` which maps every point of `Ω` to the same measure `μ` on `𝓧`. It is a Markov kernel if `μ` is a probability measure.
 
 
 # Composition

LMLTutorial/Pages/Martingales.lean

@@ -38,7 +38,7 @@ variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
 
 # Stochastic processes, filtrations, and martingales
 
-We define a measure space {lean}`Ω`, with a probability mesure {lean}`(P : Measure Ω)`.
+We define a measurable space {lean}`Ω`, with a probability measure {lean}`(P : Measure Ω)`.
 
 ```lean
 variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
@@ -86,29 +86,14 @@ 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.
+almost everywhere to a `⨆ n, 𝓕 n`-measurable function, its limit process `𝓕.limitProcess Y P`.
+This is the Mathlib lemma `Submartingale.ae_tendsto_limitProcess`.
 
 ```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
-  suffices ∃ g, StronglyMeasurable[⨆ n, 𝓕 n] g ∧ ∀ᵐ ω ∂P, Tendsto (Y · ω) atTop (𝓝 (g ω)) by
-    exact Filtration.HasLimitProcess.ae_tendsto_limitProcess this
-  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⟩
+    ∀ᵐ ω ∂P, Tendsto (Y · ω) atTop (𝓝 (𝓕.limitProcess Y P ω)) :=
+  hY.ae_tendsto_limitProcess hbdd
 ```
 
 # Stopping times
@@ -124,7 +109,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 `π`.
+stopped value of `Y` at `τ` has expectation smaller than or equal to that of its stopped value at
+`π`.
 ```lean
 example {Y : ℕ → Ω → ℝ} (hadp : StronglyAdapted 𝓕 Y)
     (hint : ∀ i, Integrable (Y i) P) :

LeanMachineLearning.lean

@@ -1,44 +1,57 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
+public import LeanMachineLearning.ForMathlib.Analysis.Complex.Exponential
 public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic
+public import LeanMachineLearning.ForMathlib.Analysis.Convex.Integral
 public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Basic
 public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv
+public import LeanMachineLearning.ForMathlib.Basic.Unique
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.ChainRule
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.CompProd
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Convex
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.DataProcessing
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.MapSequence
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Restrict
-public import LeanMachineLearning.ForMathlib.MeasureTheory.Measurable
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Group.Arithmetic
+public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Basic
+public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Constructions
 public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Embedding
+public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Instances
 public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Sigma
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.AEMeasurable
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.AbsolutelyContinuous
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.Decomposition.Lebesgue
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.Dirac
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.FiniteMeasure
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.ProbabilityMeasure
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.WithDensity
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.Lattice
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.MeasurableArg
 public import LeanMachineLearning.ForMathlib.MeasureTheory.OuterMeasure.Basic
-public import LeanMachineLearning.ForMathlib.Order.Interval.Finset
+public import LeanMachineLearning.ForMathlib.Order.Interval.Finset.Basic
+public import LeanMachineLearning.ForMathlib.Order.Interval.Finset.Nat
 public import LeanMachineLearning.ForMathlib.Probability.ConditionalProbability
 public import LeanMachineLearning.ForMathlib.Probability.HasCondDistrib
 public import LeanMachineLearning.ForMathlib.Probability.HasLaw
-public import LeanMachineLearning.ForMathlib.Probability.Independence.CondDistrib
-public import LeanMachineLearning.ForMathlib.Probability.Independence.CondIndepFun
-public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepFun
-public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepInfinitePi
-public import LeanMachineLearning.ForMathlib.Probability.Integrable
+public import LeanMachineLearning.ForMathlib.Probability.IdentDistrib
+public import LeanMachineLearning.ForMathlib.Probability.Independence.Basic
+public import LeanMachineLearning.ForMathlib.Probability.Independence.Conditional
+public import LeanMachineLearning.ForMathlib.Probability.Independence.InfinitePi
+public import LeanMachineLearning.ForMathlib.Probability.Independence.Kernel.IndepFun
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Basic
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.IntegralCompProd
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.Lemmas
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MapComap
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MeasureCompProd
+public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.WithDensity
+public import LeanMachineLearning.ForMathlib.Probability.Kernel.CondDistrib
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.IonescuTulcea.Traj
-public import LeanMachineLearning.ForMathlib.Probability.Kernel.KernelSub
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.MeasurableSpace
+public import LeanMachineLearning.ForMathlib.Probability.Kernel.RadonNikodym
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Sigma
 public import LeanMachineLearning.ForMathlib.Probability.Moments.SubExponential
 public import LeanMachineLearning.ForMathlib.Probability.Moments.SubGaussian
 public import LeanMachineLearning.ForMathlib.Probability.Process.HittingTime
-public import LeanMachineLearning.ForMathlib.Probability.WithDensity
-public import LeanMachineLearning.ForMathlib.Topology.Instances.ENNReal.Lemmas
 public import LeanMachineLearning.Online.Bandit.Algorithms.ETC
 public import LeanMachineLearning.Online.Bandit.Algorithms.Regret.BayesRegretTS
 public import LeanMachineLearning.Online.Bandit.Algorithms.Regret.ETC
@@ -47,9 +60,9 @@ public import LeanMachineLearning.Online.Bandit.Algorithms.TS
 public import LeanMachineLearning.Online.Bandit.Algorithms.UCB
 public import LeanMachineLearning.Online.Bandit.ArrayProbSpace
 public import LeanMachineLearning.Online.Bandit.BayesRegret
+public import LeanMachineLearning.Online.Bandit.Concentration
 public import LeanMachineLearning.Online.Bandit.Regret
 public import LeanMachineLearning.Online.Bandit.RewardByCountMeasure
-public import LeanMachineLearning.Online.Bandit.SumRewards
 public import LeanMachineLearning.SequentialLearning.ActionIndicator
 public import LeanMachineLearning.SequentialLearning.Algorithm
 public import LeanMachineLearning.SequentialLearning.AlgorithmDensity