diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 731b3ebc..36f3c797 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -24,3 +24,6 @@ public import LeanMachineLearning.SequentialLearning.Deterministic 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/Tutorial/BasicProbability.lean b/LeanMachineLearning/Tutorial/BasicProbability.lean new file mode 100644 index 00000000..ea63ce24 --- /dev/null +++ b/LeanMachineLearning/Tutorial/BasicProbability.lean @@ -0,0 +1,69 @@ +/- +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 + +@[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 new file mode 100644 index 00000000..a45db0dc --- /dev/null +++ b/LeanMachineLearning/Tutorial/MarkovKernel.lean @@ -0,0 +1,57 @@ +/- +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 + +@[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 + +lemma todo : 0 = 0 := rfl diff --git a/LeanMachineLearning/Tutorial/Martingales.lean b/LeanMachineLearning/Tutorial/Martingales.lean new file mode 100644 index 00000000..2808aafa --- /dev/null +++ b/LeanMachineLearning/Tutorial/Martingales.lean @@ -0,0 +1,144 @@ +/- +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 + +@[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 new file mode 100644 index 00000000..c352eec6 --- /dev/null +++ b/LeanMachineLearning/Tutorial/README.md @@ -0,0 +1,5 @@ +# 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/tutorial/Manual/Front.lean b/tutorial/Manual/Front.lean index e96bda93..e9b159e1 100644 --- a/tutorial/Manual/Front.lean +++ b/tutorial/Manual/Front.lean @@ -1,5 +1,8 @@ -import Manual.Pages.Installation +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 @@ -12,7 +15,7 @@ set_option verso.exampleModule "LeanMachineLearning" #doc (Manual) "Lean Machine Learning" => %%% -authors := ["Rémy Degenne, Paulo Rauber"] +authors := [] shortTitle := "Lean Machine Learning" %%% @@ -20,4 +23,10 @@ These tutorial pages will guide you through using the [Lean Machine Learning](ht {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/Manual/Pages/BasicProbability.lean b/tutorial/Manual/Pages/BasicProbability.lean new file mode 100644 index 00000000..5549b6f0 --- /dev/null +++ b/tutorial/Manual/Pages/BasicProbability.lean @@ -0,0 +1,121 @@ +/- + - Created in 2025 by Rémy Degenne +-/ + +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.Tutorial.BasicProbability" + +#doc (Manual) "Probability Spaces and Measures" => +%%% +htmlSplit := .never +%%% + + +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 +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 +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. +```anchor Three +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`). +```anchor Four +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. +```anchor Five +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. +```anchor Six +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/MarkovKernels.lean b/tutorial/Manual/Pages/MarkovKernels.lean new file mode 100644 index 00000000..a3d75bb1 --- /dev/null +++ b/tutorial/Manual/Pages/MarkovKernels.lean @@ -0,0 +1,92 @@ +import Manual.References +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.Tutorial.MarkovKernel" + +#doc (Manual) "Markov Kernels" => +%%% +htmlSplit := .never +%%% + +This tutorial presents a central object in our treatment of stochastic algorithms: Markov kernels, which are measurable maps between a measurable space and the probability measures on another measurable space. + +For a more in-depth exposition, see {citep Docs.degenne2025markov}[]. + +# Definition + +In probability theory, we need functions to be measurable to be able to work with them. +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 +example (κ : Kernel 𝓧 𝓨) (x : 𝓧) : Measure 𝓨 := κ x + +example (κ : Kernel 𝓧 𝓨) : Measurable κ := κ.measurable + +example (f : 𝓧 → Measure 𝓨) (hf : Measurable f) : Kernel 𝓧 𝓨 := ⟨f, hf⟩ +``` + +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 +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⟩ +``` + +Kernels arise naturally when describing the outcomes of sequential experiments. +For a toy example, suppose that if the weather is good one day, we know that it will be good the next day with probability 0.8, and if it is bad weather instead, it will be good the next day with probability 0.4. +We can describe that situation with a Markov kernel `κ` from a type with two elements `{good, bad}` to itself such that `κ good` is the probability measure giving probability 0.8 to good weather and 0.2 to bad weather, and `κ bad` is the probability measure giving probability 0.4 to good weather and 0.6 to bad weather. +On such a simple example there is no need for the measurability condition of kernels: every function from a finite set with discrete sigma-algebra to a measurable space is measurable. +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 +example (κ η : Kernel 𝓧 𝓨) : + κ = η ↔ ∀ x f, Measurable f → ∫⁻ y, f y ∂(κ x) = ∫⁻ y, f y ∂(η x) := + Kernel.ext_fun_iff +``` +Another way to show that two kernels are equal is to show that their values `κ x` and `η x` are equal for all `x`, which since they are measures can be checked by checking that they give the same value to all measurable sets. + +# Classes of kernels + +A 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. + +```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 +``` + +A measurable random variable `X : 𝓧 → 𝓨` can be seen as a `Kernel 𝓧 𝓨` that maps `ω : 𝓧` to the Dirac measure at `X ω`. +Such a kernel is called a deterministic kernel and is a Markov kernel. +It is denoted by `Kernel.deterministic X hX`, where `hX` is the measurability condition on `X`. +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 `𝓧`. + + +# Composition + +TODO: describe the various ways to compose or take products of kernels. diff --git a/tutorial/Manual/Pages/Martingales.lean b/tutorial/Manual/Pages/Martingales.lean new file mode 100644 index 00000000..2b7407a6 --- /dev/null +++ b/tutorial/Manual/Pages/Martingales.lean @@ -0,0 +1,117 @@ +/- + - Created in 2025 by Rémy Degenne +-/ + +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.Tutorial.Martingales" + +#doc (Manual) "Stochastic Processes and Martingales" => +%%% +htmlSplit := .never +%%% + +# Stochastic processes, filtrations, and martingales + +We define a measure space {anchorTerm Variables}`Ω`, with a probability mesure {anchorTerm Variables}`P : Measure Ω`. + +```anchor Variables +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} + {P : Measure Ω} [IsProbabilityMeasure P] +``` + +Let then `X` be 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} +``` + +A filtration is a monotone family of sub-σ-algebras indexed by `ℕ`. +```anchor Filtration +variable {𝓕 : Filtration ℕ mΩ} + +example : ∀ n, 𝓕 n ≤ mΩ := Filtration.le 𝓕 + +example {i j : ℕ} (hij : i ≤ j) : 𝓕 i ≤ 𝓕 j := Filtration.mono 𝓕 hij +``` + +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 +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 +``` + +*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⟩ +``` + +# 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`. + +```anchor Variables3 +variable {τ : Ω → ℕ∞} (hτ : IsStoppingTime 𝓕 τ) + +example (i : ℕ) : MeasurableSet[𝓕 i] {ω | τ ω ≤ i} := hτ.measurableSet_le i +``` + +*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⟩ +``` diff --git a/tutorial/Manual/References.lean b/tutorial/Manual/References.lean new file mode 100644 index 00000000..78b8ba8a --- /dev/null +++ b/tutorial/Manual/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