From 421a3395ce43c56008aecbff9b38f4b09d9c9a1e Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 11 Sep 2026 14:47:23 +0200 Subject: [PATCH 1/4] identification algorithm --- LeanMachineLearning.lean | 3 + .../MeasureTheory/MeasurableSpace/Sigma.lean | 75 +++ .../Probability/HasCondDistrib.lean | 30 ++ .../SequentialLearning/IdentificationAlg.lean | 191 +++++++ .../SequentialLearning/StoppedHistory.lean | 492 ++++++++++++++++++ 5 files changed, 791 insertions(+) create mode 100644 LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Sigma.lean create mode 100644 LeanMachineLearning/SequentialLearning/IdentificationAlg.lean create mode 100644 LeanMachineLearning/SequentialLearning/StoppedHistory.lean diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 4f59f7d8..662076c5 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -8,6 +8,7 @@ public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.M public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Restrict public import LeanMachineLearning.ForMathlib.MeasureTheory.Measurable public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Embedding +public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Sigma public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.AbsolutelyContinuous public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.Lattice public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.MeasurableArg @@ -57,9 +58,11 @@ public import LeanMachineLearning.SequentialLearning.DivergenceDecomposition public import LeanMachineLearning.SequentialLearning.EvaluationEnv public import LeanMachineLearning.SequentialLearning.FeedbackMartingale public import LeanMachineLearning.SequentialLearning.FiniteActions +public import LeanMachineLearning.SequentialLearning.IdentificationAlg public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace public import LeanMachineLearning.SequentialLearning.Means public import LeanMachineLearning.SequentialLearning.StationaryEnv +public import LeanMachineLearning.SequentialLearning.StoppedHistory public import LeanMachineLearning.SequentialLearning.SumRewards public import LeanMachineLearning.Tactic.EqLift public import LeanMachineLearning.Tactic.EqLift.ForMathlib.Kernel diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Sigma.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Sigma.lean new file mode 100644 index 00000000..8188af70 --- /dev/null +++ b/LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Sigma.lean @@ -0,0 +1,75 @@ +/- +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.MeasureTheory.MeasurableSpace.Embedding + +/-! +# Measurability of functions on a sigma type + +A function on `Σ a, β a` is measurable as soon as each of its restrictions `f ∘ Sigma.mk a` is. +-/ + +@[expose] public section + +open MeasurableSpace + +variable {α γ : Type*} {β : α → Type*} [∀ a, MeasurableSpace (β a)] [MeasurableSpace γ] + +@[fun_prop] +lemma measurable_sigma_mk (a : α) : Measurable (Sigma.mk a : β a → Σ a, β a) := + fun _ hs ↦ measurableSet_iInf.1 hs a + +/-- A function on a sigma type is measurable if all its restrictions to the fibers are. -/ +lemma measurable_sigma_of_measurable_comp_mk {f : (Σ a, β a) → γ} + (h : ∀ a, Measurable (f ∘ Sigma.mk a)) : Measurable f := + fun _ hs ↦ measurableSet_iInf.2 fun a ↦ (h a) hs + +/-- A set in a sigma type is measurable iff its trace on every fiber is. -/ +lemma measurableSet_sigma_iff {s : Set (Σ a, β a)} : + MeasurableSet s ↔ ∀ a, MeasurableSet (Sigma.mk a ⁻¹' s) := + measurableSet_iInf + +lemma measurable_sigma_iff {f : (Σ a, β a) → γ} : + Measurable f ↔ ∀ a, Measurable (f ∘ Sigma.mk a) := + ⟨fun hf a ↦ hf.comp (measurable_sigma_mk a), measurable_sigma_of_measurable_comp_mk⟩ + +/-- The first projection of a sigma type is measurable (it is constant on every fiber). -/ +lemma measurable_sigma_fst [MeasurableSpace α] : Measurable (Sigma.fst : (Σ a, β a) → α) := + measurable_sigma_of_measurable_comp_mk fun _ ↦ measurable_const + +/-- `x ↦ ⟨n x, f (n x) x⟩` is measurable when the index `n x` ranges over a countable type with +measurable singletons and each `f i` is measurable. -/ +lemma Measurable.sigmaMk [Countable α] [MeasurableSpace α] [MeasurableSingletonClass α] + {n : γ → α} (hn : Measurable n) {f : (a : α) → γ → β a} (hf : ∀ a, Measurable (f a)) : + Measurable fun x ↦ (⟨n x, f (n x) x⟩ : Σ a, β a) := by + intro s hs + have : (fun x ↦ (⟨n x, f (n x) x⟩ : Σ a, β a)) ⁻¹' s = + ⋃ a, n ⁻¹' {a} ∩ f a ⁻¹' (Sigma.mk a ⁻¹' s) := by + ext x + simp only [Set.mem_preimage, Set.mem_iUnion, Set.mem_inter_iff, Set.mem_singleton_iff] + constructor + · intro h + exact ⟨n x, rfl, h⟩ + · rintro ⟨a, rfl, h⟩ + exact h + rw [this] + exact MeasurableSet.iUnion fun a ↦ + (hn (measurableSet_singleton a)).inter (hf a (measurableSet_sigma_iff.1 hs a)) + +/-- `Sigma.mk a` is a measurable embedding. -/ +lemma measurableEmbedding_sigma_mk (a : α) : + MeasurableEmbedding (Sigma.mk a : β a → Σ a, β a) where + injective := sigma_mk_injective + measurable := measurable_sigma_mk a + measurableSet_image' s hs := by + rw [measurableSet_sigma_iff] + intro b + by_cases hab : a = b + · subst hab + rwa [sigma_mk_preimage_image_eq_self] + · rw [sigma_mk_preimage_image' hab] + exact MeasurableSet.empty diff --git a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean index 93e9c492..ba613ae2 100644 --- a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean +++ b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean @@ -377,4 +377,34 @@ lemma HasCondDistrib.hasCondDistrib_sectR [IsFiniteMeasure μ] [StandardBorelSpa rw [Kernel.map_apply _ hf] at ha filter_upwards [hc, ha] with b hcb hab using hcb.trans hab +/-- The restriction of `μ ⊗ₘ κ` to `s ×ˢ univ` is `μ.restrict s ⊗ₘ κ`. -/ +lemma _root_.MeasureTheory.Measure.restrict_compProd_prod_univ (μ : Measure α) [SFinite μ] + (κ : Kernel α β) [IsSFiniteKernel κ] {s : Set α} (hs : MeasurableSet s) : + (μ ⊗ₘ κ).restrict (s ×ˢ Set.univ) = μ.restrict s ⊗ₘ κ := by + ext t ht + rw [Measure.restrict_apply ht, Measure.compProd_apply (ht.inter (hs.prod MeasurableSet.univ)), + Measure.compProd_apply ht, ← lintegral_indicator hs] + refine lintegral_congr fun a ↦ ?_ + by_cases ha : a ∈ s + · have : Prod.mk a ⁻¹' (t ∩ s ×ˢ Set.univ) = Prod.mk a ⁻¹' t := by ext b; simp [ha] + simp [Set.indicator, ha, this] + · have : Prod.mk a ⁻¹' (t ∩ s ×ˢ Set.univ) = ∅ := by ext b; simp [ha] + simp [Set.indicator, ha, this] + +omit [StandardBorelSpace Ω] [Nonempty Ω] in +/-- A conditional law given `X` is a conditional law given `X` under the restriction of `P` to an +event determined by `X`. -/ +lemma HasCondDistrib.restrict_preimage [SFinite μ] [IsSFiniteKernel κ] + (hX : Measurable X) (hY : Measurable Y) + (h : HasCondDistrib Y X κ μ) {s : Set β} (hs : MeasurableSet s) : + HasCondDistrib Y X κ (μ.restrict (X ⁻¹' s)) := by + refine ⟨(hX.prodMk hY).aemeasurable, ?_⟩ + have h1 : (fun ω ↦ (X ω, Y ω)) ⁻¹' (s ×ˢ Set.univ) = X ⁻¹' s := by ext; simp + calc (μ.restrict (X ⁻¹' s)).map (fun ω ↦ (X ω, Y ω)) + = (μ.map (fun ω ↦ (X ω, Y ω))).restrict (s ×ˢ Set.univ) := by + rw [Measure.restrict_map (hX.prodMk hY) (hs.prod MeasurableSet.univ), h1] + _ = (μ.map X ⊗ₘ κ).restrict (s ×ˢ Set.univ) := by rw [h.map_eq] + _ = (μ.map X).restrict s ⊗ₘ κ := Measure.restrict_compProd_prod_univ _ _ hs + _ = (μ.restrict (X ⁻¹' s)).map X ⊗ₘ κ := by rw [Measure.restrict_map hX hs] + end ProbabilityTheory diff --git a/LeanMachineLearning/SequentialLearning/IdentificationAlg.lean b/LeanMachineLearning/SequentialLearning/IdentificationAlg.lean new file mode 100644 index 00000000..295fe645 --- /dev/null +++ b/LeanMachineLearning/SequentialLearning/IdentificationAlg.lean @@ -0,0 +1,191 @@ +/- +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 LeanMachineLearning.SequentialLearning.Deterministic +public import LeanMachineLearning.SequentialLearning.StoppedHistory + +/-! +# Identification algorithms: sampling rule, stopping rule, output rule + +An *identification algorithm* with outputs in `𝓞` is an LML sampling rule +`alg : Algorithm Unit 𝓐 𝓨` (an algorithm without observations: LML's observation type is `Unit`, +and `𝓞` denotes here the type of *outputs*) together with + +* a *stopping rule*: `stop n h` says that the algorithm stops after `n` rounds when the history + of these rounds is `h : Hist Unit 𝓐 𝓨 n` (each `{h | stop n h}` is measurable); +* an *output rule*: for each `n`, a Markov kernel `output n` from histories of length `n` to `𝓞` + (the distribution of the output when the algorithm stops after `n` rounds). + +A *run* of the algorithm in an environment `env`, on a probability space `(Ω, P)`, consists of +observation, action and feedback processes `O, X, Y` (with `O` trivially `Unit`-valued) forming an +algorithm-environment sequence for `alg` and `env` (LML `IsAlgEnvSeq`) and an output `out : Ω → 𝓞` +whose conditional law given the history at the +stopping time is the output rule (`IdentAlg.IsRun`). The stopping time `IdentAlg.stoppingTime` +is the stopping time `Learning.stoppingTime` of the stopping rule `A.stopSet` (the hitting time, +Mathlib `hittingAfter`, of the stopping rule by the process of histories), a stopping time of +the history filtration, and the history at the stopping time is `Learning.stoppedHist`. + +Examples: best-arm identification (`𝓞 = 𝓐`, output = recommended arm), hypothesis tests +(`𝓞 = Bool`), estimation (`𝓞 = ℝ`). + +A *fixed-budget* algorithm is the special case where the stopping rule is "stop after exactly +`T` rounds" (`IsFixedBudget A T`; constructor `fixedBudget alg T ρ`); a *fixed-confidence* +algorithm stops adaptively. + +## Main definitions + +* `IdentAlg 𝓐 𝓨 𝓞`: the structure. +* `IdentAlg.stoppingTime A O X Y : Ω → ℕ∞`: the number of rounds played, a hitting time. +* `IdentAlg.stoppedHist A O X Y : Ω → Σ n, Hist Unit 𝓐 𝓨 n`: the history at the stopping time. +* `IdentAlg.IsRun A env O X Y out P`: `(O, X, Y, out)` is a run of `A` in `env` on `(Ω, P)`. +* `IdentAlg.IsPAC A env good δ`: for every parameter `θ` of the family `env θ` of environments + and every run of `A` in `env θ`, the output is `good θ` with probability at least `1 - δ`. +* `IdentAlg.IsFixedBudget A T`, `IdentAlg.fixedBudget alg T ρ`: fixed-budget algorithms. +* `fixedDesignAlg x`: the deterministic algorithm playing the sequence `x` whatever the + observations; `IdentAlg.IsFixedDesign A` says that the sampling rule of `A` is of this form. + +Time is `0`-indexed: after `n` rounds the actions `a_0, …, a_{n-1}` have been played. +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory + +open scoped ENat + +universe u + +namespace Learning + +variable {𝓞 𝓐 𝓨 𝓓 Ω : Type*} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} + {m𝓞 : MeasurableSpace 𝓞} {m𝓓 : MeasurableSpace 𝓓} {mΩ : MeasurableSpace Ω} + +-- TODO: move +/-- The deterministic algorithm that plays the fixed sequence `x : ℕ → 𝓐` regardless of the +observations (a *fixed design*). -/ +noncomputable def fixedDesignAlg (x : ℕ → 𝓐) : Algorithm 𝓞 𝓐 𝓨 := + detAlgorithm (fun n _ ↦ x n) fun _ ↦ measurable_const + +/-- An identification algorithm with outputs in `𝓞`: a sampling rule `alg`, a stopping rule +`stop` (`stop n h`: stop after `n` rounds when their history is `h`) and an output rule `output` +(the distribution of the output given the history of the `n` rounds played), a Markov kernel. -/ +structure IdentAlg (𝓞 𝓐 𝓨 𝓓 : Type*) [MeasurableSpace 𝓞] [MeasurableSpace 𝓐] + [MeasurableSpace 𝓨] [MeasurableSpace 𝓓] where + /-- The sampling rule. -/ + alg : Algorithm 𝓞 𝓐 𝓨 + /-- The stopping rule: `stop n h` means that the algorithm stops after `n` rounds when the + history of these rounds is `h`. -/ + stop : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n → Prop + /-- The stopping rule is measurable. -/ + measurableSet_stop : ∀ n, MeasurableSet {h | stop n h} + /-- The output rule: distribution of the output given the history of the `n` rounds played. -/ + output : (n : ℕ) → Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓓 + /-- The output rules are Markov kernels. -/ + [isMarkovKernel_output : ∀ n, IsMarkovKernel (output n)] + +namespace IdentAlg + +variable (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) + +instance (n : ℕ) : IsMarkovKernel (A.output n) := A.isMarkovKernel_output n + +/-- The stopping time of `A` on the observation, action and feedback processes `O`, `X`, `Y`: the +number of rounds +played, that is the first `n` such that the stopping rule fires on the history of the first `n` +rounds (`⊤` if it never does). It is the stopping time `Learning.stoppingTime` of the stopping +rule `{h | A.stop h.1 h.2}`. -/ +noncomputable def stoppingTime : Ω → ℕ∞ := Learning.stoppingTime O X Y {h | A.stop h.1 h.2} + +lemma stoppingTime_def : + A.stoppingTime O X Y = Learning.stoppingTime O X Y {h | A.stop h.1 h.2} := rfl + +lemma measurableSet_stopSet : MeasurableSet {h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n | A.stop h.1 h.2} := + measurableSet_sigma_iff.2 A.measurableSet_stop + +/-- The stopping time of an identification algorithm is a stopping time of the history +filtration of any algorithm-environment sequence `X`, `Y`. -/ +lemma isStoppingTime_stoppingTime {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} + {P : Measure Ω} [IsFiniteMeasure P] (h : IsAlgEnvSeq O X Y alg env P) : + IsStoppingTime h.filtration (A.stoppingTime O X Y) := + h.isStoppingTime_stoppingTime A.measurableSet_stopSet + +/-- The history of the rounds played by `A`, as a history of variable length (of length `0` if +`A` never stops): the history stopped at `A.stoppingTime O X Y`. -/ +noncomputable def stoppedHist : Ω → Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n := + Learning.stoppedHist O X Y (A.stoppingTime O X Y) + +lemma stoppedHist_def : + A.stoppedHist O X Y = Learning.stoppedHist O X Y (A.stoppingTime O X Y) := rfl + +/-- When the stopping time is finite, the history at the stopping time belongs to the stopping +rule. -/ +lemma stoppedHist_mem_stopSet_of_ne_top {ω : Ω} (h : A.stoppingTime O X Y ω ≠ ⊤) : + A.stoppedHist O X Y ω ∈ {h | A.stop h.1 h.2} := + Learning.stoppedHist_mem_of_ne_top h + +/-- The output rule of `A` as a single kernel on histories of variable length. -/ +noncomputable def outputKernel : Kernel (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) 𝓓 where + toFun h := A.output h.1 h.2 + measurable' := measurable_sigma_of_measurable_comp_mk fun n ↦ (A.output n).measurable + +instance : IsMarkovKernel A.outputKernel := + ⟨fun h ↦ (A.isMarkovKernel_output h.1).isProbabilityMeasure h.2⟩ + +/-- `(O, X, Y, out)` is a *run* of the identification algorithm `A` in the environment `env` on +the probability space `(Ω, P)`: the observation, action and feedback processes `O`, `X`, `Y` form +an algorithm-environment sequence for the sampling rule `A.alg` and `env`, and the output `out` has +conditional law `A.output` given the history at the stopping time. -/ +structure IsRun (env : Environment 𝓞 𝓐 𝓨) (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) + (out : Ω → 𝓓) (P : Measure Ω) [IsFiniteMeasure P] : Prop where + /-- The actions and feedbacks are generated by the sampling rule in the environment. -/ + isAlgEnvSeq : IsAlgEnvSeq O X Y A.alg env P + /-- The output is drawn from the output rule applied to the history at the stopping time. -/ + hasCondDistrib_output : HasCondDistrib out (A.stoppedHist O X Y) A.outputKernel P + +/-- `A` is *PAC at level `δ`* for the family of environments `env : Θ → Environment 𝓞 𝓐 𝓨` and +the goodness predicate `good : Θ → 𝓓 → Prop` if, for every `θ` and every run of `A` in `env θ` on +a probability space `(Ω, P)`, the output is `good θ` with probability at least `1 - δ`. -/ +def IsPAC {Θ : Type*} (env : Θ → Environment 𝓞 𝓐 𝓨) (good : Θ → 𝓓 → Prop) (δ : ℝ) : Prop := + ∀ θ, ∀ {Ω : Type u} {_mΩ : MeasurableSpace Ω} (P : Measure Ω) [IsProbabilityMeasure P] + (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (out : Ω → 𝓓), + A.IsRun (env θ) O X Y out P → + 1 - δ ≤ P.real {ω | good θ (out ω)} + +/-- `A` is a *fixed-budget* algorithm with budget `T` if its stopping rule is "stop after exactly +`T` rounds". -/ +def IsFixedBudget (T : ℕ) : Prop := A.stop = fun n _ ↦ n = T + +/-- The fixed-budget identification algorithm with sampling rule `alg`, budget `T` and output +kernel `ρ` on histories of length `T` (the output rule at other lengths, never used, is an +arbitrary constant). -/ +noncomputable def fixedBudget [Nonempty 𝓓] (alg : Algorithm 𝓞 𝓐 𝓨) (T : ℕ) + (ρ : Kernel (Hist 𝓞 𝓐 𝓨 T) 𝓓) [IsMarkovKernel ρ] : IdentAlg 𝓞 𝓐 𝓨 𝓓 where + alg := alg + stop n _ := n = T + measurableSet_stop n := by by_cases h : n = T <;> simp [h] + output n := if h : n = T then ρ.comap (fun x i ↦ x (Fin.cast h.symm i)) (by fun_prop) + else Kernel.const _ (Measure.dirac (Classical.arbitrary 𝓓)) + isMarkovKernel_output n := by + by_cases h : n = T <;> simp only [h, ↓reduceDIte] <;> infer_instance + +lemma isFixedBudget_fixedBudget [Nonempty 𝓞] (alg : Algorithm Unit 𝓐 𝓨) (T : ℕ) + (ρ : Kernel (Hist Unit 𝓐 𝓨 T) 𝓞) [IsMarkovKernel ρ] : + (fixedBudget alg T ρ).IsFixedBudget T := rfl + +/-- The output rule of `fixedBudget alg T ρ` at the budget `T` is `ρ`. -/ +lemma output_fixedBudget [Nonempty 𝓞] (alg : Algorithm Unit 𝓐 𝓨) (T : ℕ) + (ρ : Kernel (Hist Unit 𝓐 𝓨 T) 𝓞) [IsMarkovKernel ρ] : + (fixedBudget alg T ρ).output T = ρ := by + change (if h : T = T then ρ.comap (fun x i ↦ x (Fin.cast h.symm i)) (by fun_prop) + else Kernel.const _ (Measure.dirac (Classical.arbitrary 𝓞))) = ρ + simp only [↓reduceDIte, Fin.cast_eq_self] + ext y u _ + simp + +end IdentAlg + +end Learning diff --git a/LeanMachineLearning/SequentialLearning/StoppedHistory.lean b/LeanMachineLearning/SequentialLearning/StoppedHistory.lean new file mode 100644 index 00000000..18ac3bc3 --- /dev/null +++ b/LeanMachineLearning/SequentialLearning/StoppedHistory.lean @@ -0,0 +1,492 @@ +/- +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 LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Sigma +public import LeanMachineLearning.SequentialLearning.Algorithm +public import Mathlib.Probability.Process.HittingTime + +/-! +# Stopping rules, stopping times and stopped histories + +A *stopping rule* is a measurable set `S : Set (Σ n, Hist 𝓞 𝓐 𝓨 n)` of histories of variable +length: the interaction stops after `n` rounds if the history of these `n` rounds belongs to +`S`. Its *stopping time* `stoppingTime O X Y S : Ω → ℕ∞` is the number of rounds played, the +hitting time (Mathlib `hittingAfter`) of `S` by the process `n ↦ ⟨n, history O X Y n⟩`. For a +random time `τ : Ω → ℕ∞`, `stoppedHist O X Y τ` is the history of the first `τ` rounds, as a +history of variable length (of length `0` if `τ = ⊤`). + +* `stoppingTime_le_iff`, `lt_stoppingTime_iff`, `stoppingTime_eq_coe_iff`, + `stoppingTime_eq_top_iff`: characterizations of the stopping time; +* `stoppedHist_mem_of_ne_top`: the stopped history belongs to `S` when the stopping time is + finite; `notMem_of_lt_stoppingTime`: the history of `n < τ` rounds does not; +* `measurable_stoppingTime`, `measurable_stoppedHist`; +* `IsAlgEnvSeq.isStoppingTime_stoppingTime`: `stoppingTime O X Y S` is a stopping time of the + history filtration of an algorithm-environment sequence; +* `exists_measurableSet_preimage_lt_stoppingTime`: the event `{n < stoppingTime O X Y S}` is + determined by the first `n` rounds; +* `truncHist M`, `truncHist_stoppedHist`: truncating the stopped history to its first `M` rounds + gives the history stopped at `min τ M`; `map_stoppedHist_min_eq_map_truncHist`: the law of + the history stopped at `min τ M` is the image of the law of the history stopped at an almost + surely finite `τ` by the truncation, and `restrict_map_truncHist`: both laws agree on histories + of length `< M`; +* `map_stoppedHist_min_eq_add`, `map_stoppedHist_min_succ_eq_add`: the laws of the histories + stopped at `min τ M` and `min τ (M + 1)` split according to whether `τ ≤ M`; + `IsAlgEnvSeq.map_history_succ_restrict_lt_stoppingTime`, + `IsAlgEnvSeq.map_history_obs_restrict_lt_stoppingTime`, + `IsAlgEnvSeq.map_action_restrict_lt_stoppingTime`: on the event `{M < τ}`, which is determined + by the first `M` rounds, the step, the observation and the action at round `M` keep their + conditional laws. + +TODO: convert lots of map_eq statements to HasLaw or HasCondDistrib. + +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory Finset + +open scoped ENat + +namespace Learning + +variable {𝓞 𝓐 𝓨 Ω : Type*} {mΩ : MeasurableSpace Ω} + +/-- The stopping time of the stopping rule `S` on the action and feedback processes `X`, `Y`: +the number of rounds played, that is the first `n` such that the history of the first `n` rounds +belongs to `S` (`⊤` if there is none). -/ +noncomputable def stoppingTime (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) + (S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) : Ω → ℕ∞ := + hittingAfter (fun n ω ↦ (⟨n, history O X Y n ω⟩ : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) S 0 + +/-- The history of the first `τ ω` rounds, as a history of variable length (of length `0` if +`τ ω = ⊤`). -/ +noncomputable def stoppedHist (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (τ : Ω → ℕ∞) + (ω : Ω) : + Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n := + ⟨(τ ω).toNat, history O X Y _ ω⟩ + +variable {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} + {τ : Ω → ℕ∞} {ω : Ω} {n M : ℕ} + +section stoppingTime + +lemma stoppingTime_le_iff : + stoppingTime O X Y S ω ≤ n ↔ ∃ j ≤ n, (⟨j, history O X Y j ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∈ S := + (hittingAfter_le_iff (u := fun n ω ↦ (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n)) + (s := S) (n := 0) (i := n) (ω := ω)).trans (by simp) + +lemma lt_stoppingTime_iff : + (n : ℕ∞) < stoppingTime O X Y S ω ↔ + ∀ j ≤ n, (⟨j, history O X Y j ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∉ S := by + rw [← not_le, stoppingTime_le_iff] + simp + +lemma stoppingTime_eq_top_iff : + stoppingTime O X Y S ω = ⊤ ↔ ∀ n, (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∉ S := + (hittingAfter_eq_top_iff (u := fun n ω ↦ (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n)) + (s := S) (n := 0) (ω := ω)).trans (by simp) + +lemma notMem_of_lt_stoppingTime (h : (n : ℕ∞) < stoppingTime O X Y S ω) : + (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∉ S := + notMem_of_lt_hittingAfter h (Nat.zero_le n) + +lemma stoppingTime_eq_coe_iff : + stoppingTime O X Y S ω = n ↔ + (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∈ S ∧ + ∀ j < n, (⟨j, history O X Y j ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∉ S := by + constructor + · intro h + refine ⟨?_, fun j hj ↦ notMem_of_lt_stoppingTime (h ▸ ENat.natCast_lt_natCast.2 hj)⟩ + obtain ⟨j, hjn, hjS⟩ := stoppingTime_le_iff.1 h.le + rcases hjn.lt_or_eq with hjn | rfl + · exact absurd hjS (notMem_of_lt_stoppingTime (h ▸ ENat.natCast_lt_natCast.2 hjn)) + · exact hjS + · rintro ⟨h1, h2⟩ + refine le_antisymm (hittingAfter_le_of_mem (Nat.zero_le n) h1) (not_lt.1 fun hlt ↦ ?_) + obtain ⟨j, hj, hjS⟩ := hittingAfter_lt_iff.1 hlt + exact h2 j hj.2 hjS + +/-- The empty stopping rule never stops. -/ +lemma stoppingTime_empty : stoppingTime O X Y (∅ : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) = fun _ ↦ ⊤ := + hittingAfter_empty 0 + +lemma stoppedHist_congr (τ τ' : Ω → ℕ∞) (h : τ ω = τ' ω) : + stoppedHist O X Y τ ω = stoppedHist O X Y τ' ω := by + unfold stoppedHist + rw [h] + +lemma stoppedHist_coe (M : ℕ) (ω : Ω) : + stoppedHist O X Y (fun _ ↦ (M : ℕ∞)) ω = ⟨M, history O X Y M ω⟩ := by + change (⟨(M : ℕ∞).toNat, history O X Y (M : ℕ∞).toNat ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) = _ + rw [ENat.toNat_natCast] + +/-- The stopped history belongs to the stopping rule when the stopping time is finite. -/ +lemma stoppedHist_mem_of_ne_top (h : stoppingTime O X Y S ω ≠ ⊤) : + stoppedHist O X Y (stoppingTime O X Y S) ω ∈ S := by + obtain ⟨n, hn⟩ := ENat.ne_top_iff_exists.1 h + rw [stoppedHist_congr (stoppingTime O X Y S) (fun _ ↦ (n : ℕ∞)) hn.symm, stoppedHist_coe] + exact (stoppingTime_eq_coe_iff.1 hn.symm).1 + +/-- If `τ ω ≤ M`, the history stopped at `min τ M` is the history stopped at `τ`. -/ +lemma stoppedHist_min_of_le (h : τ ω ≤ M) : + stoppedHist O X Y (fun ω ↦ min (τ ω) M) ω = stoppedHist O X Y τ ω := + stoppedHist_congr (fun ω ↦ min (τ ω) M) τ (min_eq_left h) + +/-- If `M < τ ω`, the history stopped at `min τ M` is the history of the first `M` rounds. -/ +lemma stoppedHist_min_of_lt (h : (M : ℕ∞) < τ ω) : + stoppedHist O X Y (fun ω ↦ min (τ ω) M) ω = ⟨M, history O X Y M ω⟩ := by + rw [stoppedHist_congr (fun ω ↦ min (τ ω) M) (fun _ ↦ (M : ℕ∞)) (min_eq_right h.le), + stoppedHist_coe] + +/-- If `M < τ ω`, the history stopped at `min τ (M + 1)` is the history of the first `M + 1` +rounds. -/ +lemma stoppedHist_min_succ_of_lt (h : (M : ℕ∞) < τ ω) : + stoppedHist O X Y (fun ω ↦ min (τ ω) (M + 1 : ℕ)) ω = ⟨M + 1, history O X Y (M + 1) ω⟩ := by + rw [stoppedHist_congr (fun ω ↦ min (τ ω) (M + 1 : ℕ)) (fun _ ↦ ((M + 1 : ℕ) : ℕ∞)) + (min_eq_right ?_), stoppedHist_coe] + exact_mod_cast Order.add_one_le_of_lt h + +/-- The history stopped at `min τ M` has length at most `M`. -/ +lemma fst_stoppedHist_min_le : (stoppedHist O X Y (fun ω ↦ min (τ ω) M) ω).1 ≤ M := + ENat.toNat_le_of_le_natCast (min_le_right _ _) + +/-- The history stopped at `min τ 0` is the empty history. -/ +lemma stoppedHist_min_zero (τ : Ω → ℕ∞) : + (stoppedHist O X Y fun ω ↦ min (τ ω) ((0 : ℕ) : ℕ∞)) = fun _ ↦ ⟨0, default⟩ := by + funext ω + rw [stoppedHist_congr (fun ω ↦ min (τ ω) ((0 : ℕ) : ℕ∞)) (fun _ ↦ ((0 : ℕ) : ℕ∞)) + (min_eq_right (by simp)), stoppedHist_coe] + exact congrArg (Sigma.mk 0) (Subsingleton.elim _ _) + +end stoppingTime + +variable {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} + +/-- The law of the history stopped at `min τ 0` is the Dirac mass at the empty history. -/ +lemma map_stoppedHist_min_zero (P : Measure Ω) [IsProbabilityMeasure P] (τ : Ω → ℕ∞) : + P.map (stoppedHist O X Y fun ω ↦ min (τ ω) ((0 : ℕ) : ℕ∞)) = + Measure.dirac (⟨0, default⟩ : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) := by + rw [stoppedHist_min_zero, Measure.map_const, measure_univ, one_smul] + +section measurableSet + +/-- The set of histories of variable length of length at most `M` is measurable. -/ +lemma measurableSet_fst_le (M : ℕ) : + MeasurableSet {h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n | h.1 ≤ M} := + measurable_sigma_fst (MeasurableSet.of_discrete (s := Set.Iic M)) + +/-- The set of histories of variable length of length less than `M` is measurable. -/ +lemma measurableSet_fst_lt (M : ℕ) : + MeasurableSet {h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n | h.1 < M} := + measurable_sigma_fst (MeasurableSet.of_discrete (s := Set.Iio M)) + +omit m𝓞 m𝓐 m𝓨 in +lemma measurable_min_natCast (hτ : Measurable τ) (M : ℕ) : + Measurable fun ω ↦ min (τ ω) (M : ℕ∞) := + (measurable_from_top (f := fun t : ℕ∞ ↦ min t M)).comp hτ + +end measurableSet + +section truncation + +/-- Truncation of a history of variable length to its first `M` rounds. -/ +def truncHist (M : ℕ) (h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n := + if hM : h.1 ≤ M then h else ⟨M, fun i ↦ h.2 (Fin.castLE (not_le.1 hM).le i)⟩ + +lemma measurable_truncHist (M : ℕ) : + Measurable (truncHist (𝓞 := 𝓞) (𝓐 := 𝓐) (𝓨 := 𝓨) M) := by + refine measurable_sigma_of_measurable_comp_mk fun n ↦ ?_ + by_cases hn : n ≤ M + · simp only [Function.comp_def, truncHist, hn, dite_true] + exact measurable_sigma_mk n + · simp only [Function.comp_def, truncHist, hn, dite_false] + exact (measurable_sigma_mk M).comp + (Measurable.of_eval fun i ↦ measurable_pi_apply (Fin.castLE (not_le.1 hn).le i)) + +omit m𝓞 m𝓐 m𝓨 in +/-- Truncating the history stopped at a finite time `τ` to its first `M` rounds gives the history +stopped at `min τ M`. -/ +lemma truncHist_stoppedHist (h : τ ω ≠ ⊤) : + truncHist M (stoppedHist O X Y τ ω) = stoppedHist O X Y (fun ω ↦ min (τ ω) M) ω := by + rcases le_or_gt (τ ω) M with hτ | hτ + · rw [stoppedHist_min_of_le hτ, truncHist, dite_eq_left] + exact ENat.toNat_le_of_le_natCast hτ + · rw [stoppedHist_min_of_lt hτ, truncHist, dite_eq_right] + · rfl + · change ¬ (τ ω).toNat ≤ M + rw [not_le, ← ENat.natCast_lt_natCast, ENat.natCast_toNat h] + exact hτ + +omit m𝓞 m𝓐 m𝓨 in +lemma truncHist_of_fst_le {h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n} (hM : h.1 ≤ M) : truncHist M h = h := + dite_eq_left hM + +omit m𝓞 m𝓐 m𝓨 in +lemma preimage_truncHist_fst_lt (M : ℕ) : + truncHist M ⁻¹' {h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n | h.1 < M} = {h | h.1 < M} := by + ext h + simp only [Set.mem_preimage, Set.mem_ofPred_eq, truncHist] + split_ifs with hM + · rfl + · simp only [lt_self_iff_false, false_iff, not_lt] + exact (not_le.1 hM).le + +/-- The image of a measure by the truncation to the first `M` rounds agrees with the measure on +histories of length `< M`. -/ +lemma restrict_map_truncHist (μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) (M : ℕ) : + (μ.map (truncHist M)).restrict {h | h.1 < M} = μ.restrict {h | h.1 < M} := by + rw [Measure.restrict_map (measurable_truncHist M) (measurableSet_fst_lt M), + preimage_truncHist_fst_lt] + conv_rhs => rw [← Measure.map_id (μ := μ.restrict {h | h.1 < M})] + refine Measure.map_congr ((ae_restrict_iff' (measurableSet_fst_lt M)).2 + (Filter.Eventually.of_forall fun h hh ↦ ?_)) + exact truncHist_of_fst_le hh.le + +end truncation + +section measurability + +variable (hO : ∀ n, Measurable (O n)) (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n)) +include hO hX hY + +lemma measurable_stoppingTime (hS : MeasurableSet S) : Measurable (stoppingTime O X Y S) := by + have hu : ∀ n, Measurable fun ω ↦ (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) := + fun n ↦ (measurable_sigma_mk n).comp (measurable_history hO hX hY n) + refine measurable_to_countable' fun x ↦ ?_ + induction x using ENat.recTopCoe with + | top => + have : stoppingTime O X Y S ⁻¹' {⊤} = + ⋂ n, (fun ω ↦ (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n)) ⁻¹' Sᶜ := by + ext ω + simp [stoppingTime_eq_top_iff] + rw [this] + exact MeasurableSet.iInter fun n ↦ hu n hS.compl + | coe n => + have : stoppingTime O X Y S ⁻¹' {(n : ℕ∞)} = + (fun ω ↦ (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n)) ⁻¹' S ∩ + ⋂ j < n, (fun ω ↦ (⟨j, history O X Y j ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n)) ⁻¹' Sᶜ := by + ext ω + simp [stoppingTime_eq_coe_iff] + rw [this] + exact (hu n hS).inter (MeasurableSet.biInter (Set.to_countable _) fun j _ ↦ hu j hS.compl) + +lemma measurableSet_stoppingTime_le (hS : MeasurableSet S) (M : ℕ) : + MeasurableSet {ω | stoppingTime O X Y S ω ≤ M} := + measurable_stoppingTime hO hX hY hS (MeasurableSet.of_discrete (s := Set.Iic (M : ℕ∞))) + +lemma measurableSet_lt_stoppingTime (hS : MeasurableSet S) (M : ℕ) : + MeasurableSet {ω | (M : ℕ∞) < stoppingTime O X Y S ω} := + measurable_stoppingTime hO hX hY hS (MeasurableSet.of_discrete (s := Set.Ioi (M : ℕ∞))) + +lemma measurable_stoppedHist (hτ : Measurable τ) : Measurable (stoppedHist O X Y τ) := + Measurable.sigmaMk (measurable_from_top.comp hτ) (measurable_history hO hX hY) + +lemma measurable_stoppedHist_min (hτ : Measurable τ) (M : ℕ) : + Measurable (stoppedHist O X Y fun ω ↦ min (τ ω) M) := + measurable_stoppedHist hO hX hY (measurable_min_natCast hτ M) + +/-- The law of the history stopped at `min τ M` is the image by the truncation to the first `M` +rounds of the law of the history stopped at an almost surely finite `τ`. -/ +lemma map_stoppedHist_min_eq_map_truncHist {P : Measure Ω} (hτ : Measurable τ) + (hτ_top : ∀ᵐ ω ∂P, τ ω ≠ ⊤) (M : ℕ) : + P.map (stoppedHist O X Y fun ω ↦ min (τ ω) M) = + (P.map (stoppedHist O X Y τ)).map (truncHist M) := by + rw [Measure.map_map (measurable_truncHist M) (measurable_stoppedHist hO hX hY hτ)] + refine Measure.map_congr ?_ + filter_upwards [hτ_top] with ω hω + exact (truncHist_stoppedHist hω).symm + +omit hO hX hY in +/-- The event `{n < stoppingTime O X Y S}` is determined by the history of the first `n` rounds. -/ +lemma exists_measurableSet_preimage_lt_stoppingTime (hS : MeasurableSet S) (n : ℕ) : + ∃ B : Set (Hist 𝓞 𝓐 𝓨 n), MeasurableSet B ∧ + {ω | (n : ℕ∞) < stoppingTime O X Y S ω} = history O X Y n ⁻¹' B := by + refine ⟨⋂ j, ⋂ (hj : j ≤ n), + {h | (⟨j, fun i ↦ h (Fin.castLE hj i)⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∉ S}, ?_, ?_⟩ + · refine MeasurableSet.iInter fun j ↦ MeasurableSet.iInter fun hj ↦ ?_ + exact ((measurable_sigma_mk j).comp (Measurable.of_eval fun _ ↦ measurable_pi_apply _)) + hS.compl + · ext ω + simp only [Set.mem_ofPred_eq, lt_stoppingTime_iff, Set.mem_preimage, Set.mem_iInter] + exact ⟨fun h j hj ↦ h j hj, fun h j hj ↦ h j hj⟩ + +end measurability + +section law + +variable (hO : ∀ n, Measurable (O n)) (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n)) + (hS : MeasurableSet S) {P : Measure Ω} +include hO hX hY hS + +omit m𝓞 m𝓐 m𝓨 hO hX hY hS in +lemma compl_setOf_stoppingTime_le : + {ω | stoppingTime O X Y S ω ≤ M}ᶜ = {ω | (M : ℕ∞) < stoppingTime O X Y S ω} := by + ext ω + simp + +/-- The law of the history stopped at `min τ M` splits according to whether `τ ≤ M`: on +`{τ ≤ M}` it is the law of the history stopped at `τ`, on `{M < τ}` it is the law of the history +of the first `M` rounds. -/ +lemma map_stoppedHist_min_eq_add (M : ℕ) : + P.map (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M) = + (P.restrict {ω | stoppingTime O X Y S ω ≤ M}).map + (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M) + + ((P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map (history O X Y M)).map + (Sigma.mk M) := by + have hZ := measurable_stoppedHist_min hO hX hY (measurable_stoppingTime hO hX hY hS) M + conv_lhs => rw [← Measure.restrict_add_restrict_compl (μ := P) + (measurableSet_stoppingTime_le hO hX hY hS M), Measure.map_add _ _ hZ, + compl_setOf_stoppingTime_le] + congr 1 + rw [Measure.map_map (measurable_sigma_mk M) (measurable_history hO hX hY M)] + refine Measure.map_congr ((ae_restrict_iff' (measurableSet_lt_stoppingTime hO hX hY hS M)).2 + (Filter.Eventually.of_forall fun ω hω ↦ ?_)) + exact stoppedHist_min_of_lt hω + +/-- The law of the history stopped at `min τ (M + 1)` splits according to whether `τ ≤ M`: on +`{τ ≤ M}` it is the law of the history stopped at `min τ M`, on `{M < τ}` it is the law of the +history of the first `M + 1` rounds. -/ +lemma map_stoppedHist_min_succ_eq_add (M : ℕ) : + P.map (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) (M + 1 : ℕ)) = + (P.restrict {ω | stoppingTime O X Y S ω ≤ M}).map + (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M) + + ((P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map (history O X Y (M + 1))).map + (Sigma.mk (M + 1)) := by + have hZ := measurable_stoppedHist_min hO hX hY (measurable_stoppingTime hO hX hY hS) (M + 1) + conv_lhs => rw [← Measure.restrict_add_restrict_compl (μ := P) + (measurableSet_stoppingTime_le hO hX hY hS M), Measure.map_add _ _ hZ, + compl_setOf_stoppingTime_le] + congr 1 + · refine Measure.map_congr ((ae_restrict_iff' (measurableSet_stoppingTime_le hO hX hY hS M)).2 + (Filter.Eventually.of_forall fun ω hω ↦ ?_)) + rw [stoppedHist_min_of_le hω, stoppedHist_min_of_le (hω.trans (by exact_mod_cast M.le_succ))] + · rw [Measure.map_map (measurable_sigma_mk (M + 1)) (measurable_history hO hX hY (M + 1))] + refine Measure.map_congr ((ae_restrict_iff' (measurableSet_lt_stoppingTime hO hX hY hS M)).2 + (Filter.Eventually.of_forall fun ω hω ↦ ?_)) + exact stoppedHist_min_succ_of_lt hω + +omit hO hX hY hS in +/-- The image of the restriction of `P` to `A` by `f` gives measure zero to a set avoided by `f` +on `A`. -/ +lemma _root_.MeasureTheory.Measure.map_restrict_apply_of_forall_notMem {H : Type*} + {mH : MeasurableSpace H} {f : Ω → H} (hf : Measurable f) {A : Set Ω} {T : Set H} + (hT : MeasurableSet T) (h : ∀ ω ∈ A, f ω ∉ T) : ((P.restrict A).map f) T = 0 := by + rw [Measure.map_apply hf hT, Measure.restrict_apply (hf hT)] + exact measure_mono_null (fun ω hω ↦ (h ω hω.2 hω.1).elim) measure_empty + +/-- On `{τ ≤ M}`, the history stopped at `min τ M` belongs to the stopping rule. -/ +lemma map_restrict_stoppingTime_le_stoppedHist_min_apply_compl (M : ℕ) : + ((P.restrict {ω | stoppingTime O X Y S ω ≤ M}).map + (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M)) Sᶜ = 0 := by + refine Measure.map_restrict_apply_of_forall_notMem + (measurable_stoppedHist_min hO hX hY (measurable_stoppingTime hO hX hY hS) M) hS.compl + fun ω hω h ↦ h ?_ + rw [stoppedHist_min_of_le hω] + exact stoppedHist_mem_of_ne_top (ne_top_of_le_ne_top (ENat.natCast_ne_top M) hω) + +/-- The history stopped at `min τ M` has length at most `M`. -/ +lemma map_restrict_stoppedHist_min_apply_compl_fst_le (A : Set Ω) (M : ℕ) : + ((P.restrict A).map (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M)) + {h | h.1 ≤ M}ᶜ = 0 := + Measure.map_restrict_apply_of_forall_notMem + (measurable_stoppedHist_min hO hX hY (measurable_stoppingTime hO hX hY hS) M) + (measurableSet_fst_le M).compl fun _ _ h ↦ h fst_stoppedHist_min_le + +/-- On `{M < τ}`, the history of the first `M` rounds does not belong to the stopping rule. -/ +lemma map_restrict_lt_stoppingTime_map_sigmaMk_apply (M : ℕ) : + (((P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map (history O X Y M)).map + (Sigma.mk M)) S = 0 := by + rw [Measure.map_map (measurable_sigma_mk M) (measurable_history hO hX hY M)] + exact Measure.map_restrict_apply_of_forall_notMem + ((measurable_sigma_mk M).comp (measurable_history hO hX hY M)) hS + fun ω hω ↦ notMem_of_lt_stoppingTime hω + +omit hO hX hY hS in +/-- A history of length `M + 1` does not have length at most `M`. -/ +lemma map_sigmaMk_succ_apply_fst_le (μ : Measure (Hist 𝓞 𝓐 𝓨 (M + 1))) : + (μ.map (Sigma.mk (M + 1))) {h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n | h.1 ≤ M} = 0 := by + rw [Measure.map_apply (measurable_sigma_mk (M + 1)) (measurableSet_fst_le M)] + have : Sigma.mk (M + 1) ⁻¹' {h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n | h.1 ≤ M} = ∅ := by + ext h + simp + rw [this, measure_empty] + +end law + +section filtration + +variable {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : Measure Ω} [IsFiniteMeasure P] + +lemma IsAlgEnvSeq.adapted_sigmaHistory (h : IsAlgEnvSeq O X Y alg env P) : + Adapted h.filtration + (fun n ω ↦ (⟨n, history O X Y n ω⟩ : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) := + fun n ↦ (measurable_sigma_mk n).comp (h.adapted_history n) + +/-- The stopping time of a stopping rule is a stopping time of the history filtration of any +algorithm-environment sequence. -/ +lemma IsAlgEnvSeq.isStoppingTime_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) + (hS : MeasurableSet S) : + IsStoppingTime h.filtration (stoppingTime O X Y S) := + h.adapted_sigmaHistory.isStoppingTime_hittingAfter hS + +/-- On the event `{M < τ}`, which is determined by the first `M` rounds, the step at round `M` +keeps its conditional law given the first `M` rounds. -/ +lemma IsAlgEnvSeq.hasCondDistrib_step_restrict_lt_stoppingTime + (h : IsAlgEnvSeq O X Y alg env P) (hS : MeasurableSet S) (M : ℕ) : + HasCondDistrib (step O X Y M) (history O X Y M) (stepKernel alg env M) + (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) := by + obtain ⟨B, hB, hB_eq⟩ := + exists_measurableSet_preimage_lt_stoppingTime (O := O) (X := X) (Y := Y) hS M + rw [hB_eq] + exact (h.hasCondDistrib_step M).restrict_preimage + (h.measurable_history M) (h.measurable_step M) hB + +/-- On the event `{M < τ}`, the law of the first `M + 1` rounds is the composition-product of +the law of the first `M` rounds with the step kernel. -/ +lemma IsAlgEnvSeq.map_history_succ_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) + (hS : MeasurableSet S) (M : ℕ) : + (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map (history O X Y (M + 1)) = + ((P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map (history O X Y M) ⊗ₘ + stepKernel alg env M).map ((MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) M).symm) := by + rw [history_succ, ← (h.hasCondDistrib_step_restrict_lt_stoppingTime hS M).map_eq, + Measure.map_map (MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) _).symm.measurable] + exact (h.measurable_history _).prodMk (h.measurable_step _) + +/-- On the event `{M < τ}`, the law of the first `M` rounds together with the observation at +round `M` is the composition-product of the law of the first `M` rounds with the observation +kernel. -/ +lemma IsAlgEnvSeq.map_history_obs_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) + (hS : MeasurableSet S) (M : ℕ) : + (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map + (fun ω ↦ (history O X Y M ω, O M ω)) = + (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map (history O X Y M) ⊗ₘ env.obs M := by + obtain ⟨B, hB, hB_eq⟩ := + exists_measurableSet_preimage_lt_stoppingTime (O := O) (X := X) (Y := Y) hS M + rw [hB_eq] + exact ((h.hasCondDistrib_obs M).restrict_preimage (h.measurable_history M) (h.measurable_obs M) + hB).map_eq + +/-- On the event `{M < τ}`, the law of the action at round `M` is the policy applied to the law +of the first `M` rounds and of the observation at round `M`. -/ +lemma IsAlgEnvSeq.map_action_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) + (hS : MeasurableSet S) (M : ℕ) : + (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map (X M) = + alg.policy M ∘ₘ (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map + (fun ω ↦ (history O X Y M ω, O M ω)) := by + obtain ⟨B, hB, hB_eq⟩ := + exists_measurableSet_preimage_lt_stoppingTime (O := O) (X := X) (Y := Y) hS M + have hB' : history O X Y M ⁻¹' B = (fun ω ↦ (history O X Y M ω, O M ω)) ⁻¹' (B ×ˢ Set.univ) := by + ext ω + simp + rw [hB_eq, hB'] + exact ((h.hasCondDistrib_action M).restrict_preimage + ((h.measurable_history M).prodMk (h.measurable_obs M)) (h.measurable_action M) + (hB.prod MeasurableSet.univ)).hasLaw_comp.map_eq + +end filtration + +end Learning From 062c0c65e0c86be598cebc3b60bc25effc29a513 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 11 Sep 2026 15:07:02 +0200 Subject: [PATCH 2/4] use HasLaw/HasCondDistrib; remove truncHist --- .../ForMathlib/Probability/HasLaw.lean | 32 ++ .../SequentialLearning/StoppedHistory.lean | 275 +++++++----------- 2 files changed, 130 insertions(+), 177 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/Probability/HasLaw.lean b/LeanMachineLearning/ForMathlib/Probability/HasLaw.lean index b8c69102..7e333267 100644 --- a/LeanMachineLearning/ForMathlib/Probability/HasLaw.lean +++ b/LeanMachineLearning/ForMathlib/Probability/HasLaw.lean @@ -29,6 +29,38 @@ lemma _root_.AEMeasurable.hasLaw_map {X : Ω → 𝓧} (hX : AEMeasurable X P) : lemma _root_.Measurable.hasLaw_map {X : Ω → 𝓧} (hX : Measurable X) (P : Measure Ω) : HasLaw X (P.map X) P := ⟨hX.aemeasurable, rfl⟩ +section Restrict + +variable {X : Ω → 𝓧} {μ ν : Measure 𝓧} + +/-- If a random variable with law `μ` almost surely does not belong to a measurable set `T`, then +`μ T = 0`. -/ +lemma HasLaw.measure_eq_zero_of_ae_notMem (h : HasLaw X μ P) {T : Set 𝓧} (hT : MeasurableSet T) + (hXT : ∀ᵐ ω ∂P, X ω ∉ T) : + μ T = 0 := by + rw [← h.map_eq, Measure.map_apply_of_aemeasurable h.aemeasurable hT, + measure_eq_zero_iff_ae_notMem] + exact hXT + +/-- If `X` has law `μ` under the restriction of `P` to a measurable set `s` and law `ν` under the +restriction of `P` to `sᶜ`, then `X` has law `μ + ν` under `P`. -/ +lemma HasLaw.add_of_restrict_compl {s : Set Ω} (hs : MeasurableSet s) + (hμ : HasLaw X μ (P.restrict s)) (hν : HasLaw X ν (P.restrict sᶜ)) : + HasLaw X (μ + ν) P := by + have hX : AEMeasurable X P := by + rw [← Measure.restrict_add_restrict_compl (μ := P) hs, aemeasurable_add_measure_iff] + exact ⟨hμ.aemeasurable, hν.aemeasurable⟩ + refine ⟨hX, ?_⟩ + calc P.map X = (P.restrict s + P.restrict sᶜ).map (hX.mk X) := by + rw [Measure.restrict_add_restrict_compl hs, Measure.map_congr hX.ae_eq_mk] + _ = (P.restrict s).map X + (P.restrict sᶜ).map X := by + rw [Measure.map_add _ _ hX.measurable_mk, + Measure.map_congr (ae_restrict_of_ae (s := s) hX.ae_eq_mk), + Measure.map_congr (ae_restrict_of_ae (s := sᶜ) hX.ae_eq_mk)] + _ = μ + ν := by rw [hμ.map_eq, hν.map_eq] + +end Restrict + section Cond variable {ι : Type*} [Countable ι] {mι : MeasurableSpace ι} [MeasurableSingletonClass ι] diff --git a/LeanMachineLearning/SequentialLearning/StoppedHistory.lean b/LeanMachineLearning/SequentialLearning/StoppedHistory.lean index 18ac3bc3..e098c529 100644 --- a/LeanMachineLearning/SequentialLearning/StoppedHistory.lean +++ b/LeanMachineLearning/SequentialLearning/StoppedHistory.lean @@ -6,6 +6,7 @@ Authors: Rémy Degenne module public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Sigma +public import LeanMachineLearning.ForMathlib.Probability.HasLaw public import LeanMachineLearning.SequentialLearning.Algorithm public import Mathlib.Probability.Process.HittingTime @@ -28,20 +29,15 @@ history of variable length (of length `0` if `τ = ⊤`). history filtration of an algorithm-environment sequence; * `exists_measurableSet_preimage_lt_stoppingTime`: the event `{n < stoppingTime O X Y S}` is determined by the first `n` rounds; -* `truncHist M`, `truncHist_stoppedHist`: truncating the stopped history to its first `M` rounds - gives the history stopped at `min τ M`; `map_stoppedHist_min_eq_map_truncHist`: the law of - the history stopped at `min τ M` is the image of the law of the history stopped at an almost - surely finite `τ` by the truncation, and `restrict_map_truncHist`: both laws agree on histories - of length `< M`; -* `map_stoppedHist_min_eq_add`, `map_stoppedHist_min_succ_eq_add`: the laws of the histories +* `hasLaw_stoppedHist_min_add`, `hasLaw_stoppedHist_min_succ_add`: the laws of the histories stopped at `min τ M` and `min τ (M + 1)` split according to whether `τ ≤ M`; - `IsAlgEnvSeq.map_history_succ_restrict_lt_stoppingTime`, - `IsAlgEnvSeq.map_history_obs_restrict_lt_stoppingTime`, - `IsAlgEnvSeq.map_action_restrict_lt_stoppingTime`: on the event `{M < τ}`, which is determined - by the first `M` rounds, the step, the observation and the action at round `M` keep their - conditional laws. - -TODO: convert lots of map_eq statements to HasLaw or HasCondDistrib. + `IsAlgEnvSeq.hasCondDistrib_step_restrict_lt_stoppingTime`, + `IsAlgEnvSeq.hasCondDistrib_obs_restrict_lt_stoppingTime`, + `IsAlgEnvSeq.hasCondDistrib_action_restrict_lt_stoppingTime`: on the event `{M < τ}`, which is + determined by the first `M` rounds, the step, the observation and the action at round `M` keep + their conditional laws; `IsAlgEnvSeq.hasLaw_history_succ_restrict_lt_stoppingTime`: on this + event, the law of the first `M + 1` rounds is the composition-product of the law of the first + `M` rounds with the step kernel. -/ @@ -166,11 +162,12 @@ end stoppingTime variable {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} -/-- The law of the history stopped at `min τ 0` is the Dirac mass at the empty history. -/ -lemma map_stoppedHist_min_zero (P : Measure Ω) [IsProbabilityMeasure P] (τ : Ω → ℕ∞) : - P.map (stoppedHist O X Y fun ω ↦ min (τ ω) ((0 : ℕ) : ℕ∞)) = - Measure.dirac (⟨0, default⟩ : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) := by - rw [stoppedHist_min_zero, Measure.map_const, measure_univ, one_smul] +/-- The history stopped at `min τ 0` has law the Dirac mass at the empty history. -/ +lemma hasLaw_stoppedHist_min_zero (P : Measure Ω) [IsProbabilityMeasure P] (τ : Ω → ℕ∞) : + HasLaw (stoppedHist O X Y fun ω ↦ min (τ ω) ((0 : ℕ) : ℕ∞)) + (Measure.dirac (⟨0, default⟩ : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) P := by + rw [stoppedHist_min_zero] + exact hasLaw_dirac_of_ae_eq (ae_eq_refl _) section measurableSet @@ -191,63 +188,6 @@ lemma measurable_min_natCast (hτ : Measurable τ) (M : ℕ) : end measurableSet -section truncation - -/-- Truncation of a history of variable length to its first `M` rounds. -/ -def truncHist (M : ℕ) (h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n := - if hM : h.1 ≤ M then h else ⟨M, fun i ↦ h.2 (Fin.castLE (not_le.1 hM).le i)⟩ - -lemma measurable_truncHist (M : ℕ) : - Measurable (truncHist (𝓞 := 𝓞) (𝓐 := 𝓐) (𝓨 := 𝓨) M) := by - refine measurable_sigma_of_measurable_comp_mk fun n ↦ ?_ - by_cases hn : n ≤ M - · simp only [Function.comp_def, truncHist, hn, dite_true] - exact measurable_sigma_mk n - · simp only [Function.comp_def, truncHist, hn, dite_false] - exact (measurable_sigma_mk M).comp - (Measurable.of_eval fun i ↦ measurable_pi_apply (Fin.castLE (not_le.1 hn).le i)) - -omit m𝓞 m𝓐 m𝓨 in -/-- Truncating the history stopped at a finite time `τ` to its first `M` rounds gives the history -stopped at `min τ M`. -/ -lemma truncHist_stoppedHist (h : τ ω ≠ ⊤) : - truncHist M (stoppedHist O X Y τ ω) = stoppedHist O X Y (fun ω ↦ min (τ ω) M) ω := by - rcases le_or_gt (τ ω) M with hτ | hτ - · rw [stoppedHist_min_of_le hτ, truncHist, dite_eq_left] - exact ENat.toNat_le_of_le_natCast hτ - · rw [stoppedHist_min_of_lt hτ, truncHist, dite_eq_right] - · rfl - · change ¬ (τ ω).toNat ≤ M - rw [not_le, ← ENat.natCast_lt_natCast, ENat.natCast_toNat h] - exact hτ - -omit m𝓞 m𝓐 m𝓨 in -lemma truncHist_of_fst_le {h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n} (hM : h.1 ≤ M) : truncHist M h = h := - dite_eq_left hM - -omit m𝓞 m𝓐 m𝓨 in -lemma preimage_truncHist_fst_lt (M : ℕ) : - truncHist M ⁻¹' {h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n | h.1 < M} = {h | h.1 < M} := by - ext h - simp only [Set.mem_preimage, Set.mem_ofPred_eq, truncHist] - split_ifs with hM - · rfl - · simp only [lt_self_iff_false, false_iff, not_lt] - exact (not_le.1 hM).le - -/-- The image of a measure by the truncation to the first `M` rounds agrees with the measure on -histories of length `< M`. -/ -lemma restrict_map_truncHist (μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) (M : ℕ) : - (μ.map (truncHist M)).restrict {h | h.1 < M} = μ.restrict {h | h.1 < M} := by - rw [Measure.restrict_map (measurable_truncHist M) (measurableSet_fst_lt M), - preimage_truncHist_fst_lt] - conv_rhs => rw [← Measure.map_id (μ := μ.restrict {h | h.1 < M})] - refine Measure.map_congr ((ae_restrict_iff' (measurableSet_fst_lt M)).2 - (Filter.Eventually.of_forall fun h hh ↦ ?_)) - exact truncHist_of_fst_le hh.le - -end truncation - section measurability variable (hO : ∀ n, Measurable (O n)) (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n)) @@ -289,17 +229,6 @@ lemma measurable_stoppedHist_min (hτ : Measurable τ) (M : ℕ) : Measurable (stoppedHist O X Y fun ω ↦ min (τ ω) M) := measurable_stoppedHist hO hX hY (measurable_min_natCast hτ M) -/-- The law of the history stopped at `min τ M` is the image by the truncation to the first `M` -rounds of the law of the history stopped at an almost surely finite `τ`. -/ -lemma map_stoppedHist_min_eq_map_truncHist {P : Measure Ω} (hτ : Measurable τ) - (hτ_top : ∀ᵐ ω ∂P, τ ω ≠ ⊤) (M : ℕ) : - P.map (stoppedHist O X Y fun ω ↦ min (τ ω) M) = - (P.map (stoppedHist O X Y τ)).map (truncHist M) := by - rw [Measure.map_map (measurable_truncHist M) (measurable_stoppedHist hO hX hY hτ)] - refine Measure.map_congr ?_ - filter_upwards [hτ_top] with ω hω - exact (truncHist_stoppedHist hω).symm - omit hO hX hY in /-- The event `{n < stoppingTime O X Y S}` is determined by the history of the first `n` rounds. -/ lemma exists_measurableSet_preimage_lt_stoppingTime (hS : MeasurableSet S) (n : ℕ) : @@ -329,81 +258,76 @@ lemma compl_setOf_stoppingTime_le : simp /-- The law of the history stopped at `min τ M` splits according to whether `τ ≤ M`: on -`{τ ≤ M}` it is the law of the history stopped at `τ`, on `{M < τ}` it is the law of the history -of the first `M` rounds. -/ -lemma map_stoppedHist_min_eq_add (M : ℕ) : - P.map (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M) = - (P.restrict {ω | stoppingTime O X Y S ω ≤ M}).map - (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M) + - ((P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map (history O X Y M)).map - (Sigma.mk M) := by - have hZ := measurable_stoppedHist_min hO hX hY (measurable_stoppingTime hO hX hY hS) M - conv_lhs => rw [← Measure.restrict_add_restrict_compl (μ := P) - (measurableSet_stoppingTime_le hO hX hY hS M), Measure.map_add _ _ hZ, - compl_setOf_stoppingTime_le] - congr 1 - rw [Measure.map_map (measurable_sigma_mk M) (measurable_history hO hX hY M)] - refine Measure.map_congr ((ae_restrict_iff' (measurableSet_lt_stoppingTime hO hX hY hS M)).2 - (Filter.Eventually.of_forall fun ω hω ↦ ?_)) +`{τ ≤ M}` it is the law of the history stopped at `τ` (or equivalently at `min τ M`), on +`{M < τ}` it is the law of the history of the first `M` rounds. -/ +lemma hasLaw_stoppedHist_min_add {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} + {ν : Measure (Hist 𝓞 𝓐 𝓨 M)} + (hμ : HasLaw (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M) μ + (P.restrict {ω | stoppingTime O X Y S ω ≤ M})) + (hν : HasLaw (history O X Y M) ν (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω})) : + HasLaw (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M) + (μ + ν.map (Sigma.mk M)) P := by + refine hμ.add_of_restrict_compl (measurableSet_stoppingTime_le hO hX hY hS M) ?_ + rw [compl_setOf_stoppingTime_le] + refine (((measurable_sigma_mk M).hasLaw_map ν).comp hν).congr + ((ae_restrict_iff' (measurableSet_lt_stoppingTime hO hX hY hS M)).2 + (Filter.Eventually.of_forall fun ω hω ↦ ?_)) exact stoppedHist_min_of_lt hω /-- The law of the history stopped at `min τ (M + 1)` splits according to whether `τ ≤ M`: on `{τ ≤ M}` it is the law of the history stopped at `min τ M`, on `{M < τ}` it is the law of the history of the first `M + 1` rounds. -/ -lemma map_stoppedHist_min_succ_eq_add (M : ℕ) : - P.map (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) (M + 1 : ℕ)) = - (P.restrict {ω | stoppingTime O X Y S ω ≤ M}).map - (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M) + - ((P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map (history O X Y (M + 1))).map - (Sigma.mk (M + 1)) := by - have hZ := measurable_stoppedHist_min hO hX hY (measurable_stoppingTime hO hX hY hS) (M + 1) - conv_lhs => rw [← Measure.restrict_add_restrict_compl (μ := P) - (measurableSet_stoppingTime_le hO hX hY hS M), Measure.map_add _ _ hZ, - compl_setOf_stoppingTime_le] - congr 1 - · refine Measure.map_congr ((ae_restrict_iff' (measurableSet_stoppingTime_le hO hX hY hS M)).2 +lemma hasLaw_stoppedHist_min_succ_add {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} + {ν : Measure (Hist 𝓞 𝓐 𝓨 (M + 1))} + (hμ : HasLaw (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M) μ + (P.restrict {ω | stoppingTime O X Y S ω ≤ M})) + (hν : HasLaw (history O X Y (M + 1)) ν + (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω})) : + HasLaw (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) (M + 1 : ℕ)) + (μ + ν.map (Sigma.mk (M + 1))) P := by + refine HasLaw.add_of_restrict_compl (measurableSet_stoppingTime_le hO hX hY hS M) ?_ ?_ + · refine hμ.congr ((ae_restrict_iff' (measurableSet_stoppingTime_le hO hX hY hS M)).2 (Filter.Eventually.of_forall fun ω hω ↦ ?_)) rw [stoppedHist_min_of_le hω, stoppedHist_min_of_le (hω.trans (by exact_mod_cast M.le_succ))] - · rw [Measure.map_map (measurable_sigma_mk (M + 1)) (measurable_history hO hX hY (M + 1))] - refine Measure.map_congr ((ae_restrict_iff' (measurableSet_lt_stoppingTime hO hX hY hS M)).2 - (Filter.Eventually.of_forall fun ω hω ↦ ?_)) + · rw [compl_setOf_stoppingTime_le] + refine (((measurable_sigma_mk (M + 1)).hasLaw_map ν).comp hν).congr + ((ae_restrict_iff' (measurableSet_lt_stoppingTime hO hX hY hS M)).2 + (Filter.Eventually.of_forall fun ω hω ↦ ?_)) exact stoppedHist_min_succ_of_lt hω -omit hO hX hY hS in -/-- The image of the restriction of `P` to `A` by `f` gives measure zero to a set avoided by `f` -on `A`. -/ -lemma _root_.MeasureTheory.Measure.map_restrict_apply_of_forall_notMem {H : Type*} - {mH : MeasurableSpace H} {f : Ω → H} (hf : Measurable f) {A : Set Ω} {T : Set H} - (hT : MeasurableSet T) (h : ∀ ω ∈ A, f ω ∉ T) : ((P.restrict A).map f) T = 0 := by - rw [Measure.map_apply hf hT, Measure.restrict_apply (hf hT)] - exact measure_mono_null (fun ω hω ↦ (h ω hω.2 hω.1).elim) measure_empty - -/-- On `{τ ≤ M}`, the history stopped at `min τ M` belongs to the stopping rule. -/ -lemma map_restrict_stoppingTime_le_stoppedHist_min_apply_compl (M : ℕ) : - ((P.restrict {ω | stoppingTime O X Y S ω ≤ M}).map - (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M)) Sᶜ = 0 := by - refine Measure.map_restrict_apply_of_forall_notMem - (measurable_stoppedHist_min hO hX hY (measurable_stoppingTime hO hX hY hS) M) hS.compl - fun ω hω h ↦ h ?_ +/-- On `{τ ≤ M}`, the history stopped at `min τ M` belongs to the stopping rule: its law under +the restriction of `P` to `{τ ≤ M}` gives measure zero to `Sᶜ`. -/ +lemma _root_.ProbabilityTheory.HasLaw.stoppedHist_min_restrict_stoppingTime_le_apply_compl + {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} + (hμ : HasLaw (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M) μ + (P.restrict {ω | stoppingTime O X Y S ω ≤ M})) : + μ Sᶜ = 0 := by + refine hμ.measure_eq_zero_of_ae_notMem hS.compl + ((ae_restrict_iff' (measurableSet_stoppingTime_le hO hX hY hS M)).2 + (Filter.Eventually.of_forall fun ω hω h ↦ h ?_)) rw [stoppedHist_min_of_le hω] exact stoppedHist_mem_of_ne_top (ne_top_of_le_ne_top (ENat.natCast_ne_top M) hω) -/-- The history stopped at `min τ M` has length at most `M`. -/ -lemma map_restrict_stoppedHist_min_apply_compl_fst_le (A : Set Ω) (M : ℕ) : - ((P.restrict A).map (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M)) - {h | h.1 ≤ M}ᶜ = 0 := - Measure.map_restrict_apply_of_forall_notMem - (measurable_stoppedHist_min hO hX hY (measurable_stoppingTime hO hX hY hS) M) - (measurableSet_fst_le M).compl fun _ _ h ↦ h fst_stoppedHist_min_le - -/-- On `{M < τ}`, the history of the first `M` rounds does not belong to the stopping rule. -/ -lemma map_restrict_lt_stoppingTime_map_sigmaMk_apply (M : ℕ) : - (((P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map (history O X Y M)).map - (Sigma.mk M)) S = 0 := by - rw [Measure.map_map (measurable_sigma_mk M) (measurable_history hO hX hY M)] - exact Measure.map_restrict_apply_of_forall_notMem - ((measurable_sigma_mk M).comp (measurable_history hO hX hY M)) hS - fun ω hω ↦ notMem_of_lt_stoppingTime hω +omit hO hX hY hS in +/-- The history stopped at `min τ M` has length at most `M`: its law gives measure zero to the +histories of length `> M`. -/ +lemma _root_.ProbabilityTheory.HasLaw.stoppedHist_min_apply_compl_fst_le + {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} + (hμ : HasLaw (stoppedHist O X Y fun ω ↦ min (τ ω) M) μ P) : + μ {h | h.1 ≤ M}ᶜ = 0 := + hμ.measure_eq_zero_of_ae_notMem (measurableSet_fst_le M).compl + (ae_of_all _ fun _ h ↦ h fst_stoppedHist_min_le) + +/-- On `{M < τ}`, the history of the first `M` rounds does not belong to the stopping rule: if it +has law `ν` under the restriction of `P` to `{M < τ}`, the image of `ν` by `Sigma.mk M` gives +measure zero to `S`. -/ +lemma _root_.ProbabilityTheory.HasLaw.history_restrict_lt_stoppingTime_map_sigmaMk_apply + {ν : Measure (Hist 𝓞 𝓐 𝓨 M)} + (hν : HasLaw (history O X Y M) ν (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω})) : + (ν.map (Sigma.mk M)) S = 0 := + (((measurable_sigma_mk M).hasLaw_map ν).comp hν).measure_eq_zero_of_ae_notMem hS + ((ae_restrict_iff' (measurableSet_lt_stoppingTime hO hX hY hS M)).2 + (Filter.Eventually.of_forall fun _ hω ↦ notMem_of_lt_stoppingTime hω)) omit hO hX hY hS in /-- A history of length `M + 1` does not have length at most `M`. -/ @@ -445,47 +369,44 @@ lemma IsAlgEnvSeq.hasCondDistrib_step_restrict_lt_stoppingTime exact (h.hasCondDistrib_step M).restrict_preimage (h.measurable_history M) (h.measurable_step M) hB -/-- On the event `{M < τ}`, the law of the first `M + 1` rounds is the composition-product of -the law of the first `M` rounds with the step kernel. -/ -lemma IsAlgEnvSeq.map_history_succ_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) - (hS : MeasurableSet S) (M : ℕ) : - (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map (history O X Y (M + 1)) = - ((P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map (history O X Y M) ⊗ₘ - stepKernel alg env M).map ((MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) M).symm) := by - rw [history_succ, ← (h.hasCondDistrib_step_restrict_lt_stoppingTime hS M).map_eq, - Measure.map_map (MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) _).symm.measurable] - exact (h.measurable_history _).prodMk (h.measurable_step _) - -/-- On the event `{M < τ}`, the law of the first `M` rounds together with the observation at -round `M` is the composition-product of the law of the first `M` rounds with the observation -kernel. -/ -lemma IsAlgEnvSeq.map_history_obs_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) +/-- On the event `{M < τ}`, if the first `M` rounds have law `μ`, the first `M + 1` rounds have +law the composition-product of `μ` with the step kernel. -/ +lemma IsAlgEnvSeq.hasLaw_history_succ_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) + (hS : MeasurableSet S) {μ : Measure (Hist 𝓞 𝓐 𝓨 M)} + (hμ : HasLaw (history O X Y M) μ (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω})) : + HasLaw (history O X Y (M + 1)) + ((μ ⊗ₘ stepKernel alg env M).map (MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) M).symm) + (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) := by + rw [history_succ] + exact ((MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) M).symm.measurable.hasLaw_map _).comp + (hμ.prodMk_of_hasCondDistrib (h.hasCondDistrib_step_restrict_lt_stoppingTime hS M)) + +/-- On the event `{M < τ}`, which is determined by the first `M` rounds, the observation at round +`M` keeps its conditional law given the first `M` rounds. -/ +lemma IsAlgEnvSeq.hasCondDistrib_obs_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) (hS : MeasurableSet S) (M : ℕ) : - (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map - (fun ω ↦ (history O X Y M ω, O M ω)) = - (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map (history O X Y M) ⊗ₘ env.obs M := by + HasCondDistrib (O M) (history O X Y M) (env.obs M) + (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) := by obtain ⟨B, hB, hB_eq⟩ := exists_measurableSet_preimage_lt_stoppingTime (O := O) (X := X) (Y := Y) hS M rw [hB_eq] - exact ((h.hasCondDistrib_obs M).restrict_preimage (h.measurable_history M) (h.measurable_obs M) - hB).map_eq + exact (h.hasCondDistrib_obs M).restrict_preimage (h.measurable_history M) (h.measurable_obs M) hB -/-- On the event `{M < τ}`, the law of the action at round `M` is the policy applied to the law -of the first `M` rounds and of the observation at round `M`. -/ -lemma IsAlgEnvSeq.map_action_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) +/-- On the event `{M < τ}`, which is determined by the first `M` rounds, the action at round `M` +keeps its conditional law given the first `M` rounds and the observation at round `M`. -/ +lemma IsAlgEnvSeq.hasCondDistrib_action_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) (hS : MeasurableSet S) (M : ℕ) : - (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map (X M) = - alg.policy M ∘ₘ (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}).map - (fun ω ↦ (history O X Y M ω, O M ω)) := by + HasCondDistrib (X M) (fun ω ↦ (history O X Y M ω, O M ω)) (alg.policy M) + (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) := by obtain ⟨B, hB, hB_eq⟩ := exists_measurableSet_preimage_lt_stoppingTime (O := O) (X := X) (Y := Y) hS M have hB' : history O X Y M ⁻¹' B = (fun ω ↦ (history O X Y M ω, O M ω)) ⁻¹' (B ×ˢ Set.univ) := by ext ω simp rw [hB_eq, hB'] - exact ((h.hasCondDistrib_action M).restrict_preimage + exact (h.hasCondDistrib_action M).restrict_preimage ((h.measurable_history M).prodMk (h.measurable_obs M)) (h.measurable_action M) - (hB.prod MeasurableSet.univ)).hasLaw_comp.map_eq + (hB.prod MeasurableSet.univ) end filtration From ad6c10a4bcdb5c4d0896fcc1de5e60a41113429b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 12 Sep 2026 07:44:13 +0200 Subject: [PATCH 3/4] refactor --- LeanMachineLearning.lean | 1 + .../MeasureTheory/MeasurableSpace/Sigma.lean | 28 +- .../Probability/HasCondDistrib.lean | 10 + .../ForMathlib/Probability/Kernel/Sigma.lean | 44 ++ .../SequentialLearning/Algorithm.lean | 12 + .../SequentialLearning/Deterministic.lean | 16 + .../SequentialLearning/IdentificationAlg.lean | 263 +++++++----- .../SequentialLearning/StoppedHistory.lean | 385 ++++++++++-------- 8 files changed, 476 insertions(+), 283 deletions(-) create mode 100644 LeanMachineLearning/ForMathlib/Probability/Kernel/Sigma.lean diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 662076c5..1f86e0cd 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -30,6 +30,7 @@ public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.Meas 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.Sigma public import LeanMachineLearning.ForMathlib.Probability.Moments.SubExponential public import LeanMachineLearning.ForMathlib.Probability.Moments.SubGaussian public import LeanMachineLearning.ForMathlib.Probability.WithDensity diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Sigma.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Sigma.lean index 8188af70..a41b1f2b 100644 --- a/LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Sigma.lean +++ b/LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Sigma.lean @@ -6,16 +6,18 @@ Authors: Rémy Degenne module public import Mathlib.MeasureTheory.MeasurableSpace.Embedding +public import Mathlib.MeasureTheory.Measure.Map /-! # Measurability of functions on a sigma type A function on `Σ a, β a` is measurable as soon as each of its restrictions `f ∘ Sigma.mk a` is. +We also record measurability facts about the first projection of `Σ n : ℕ, β n`. -/ @[expose] public section -open MeasurableSpace +open MeasurableSpace MeasureTheory variable {α γ : Type*} {β : α → Type*} [∀ a, MeasurableSpace (β a)] [MeasurableSpace γ] @@ -73,3 +75,27 @@ lemma measurableEmbedding_sigma_mk (a : α) : rwa [sigma_mk_preimage_image_eq_self] · rw [sigma_mk_preimage_image' hab] exact MeasurableSet.empty + +section Nat + +variable {X : ℕ → Type*} [∀ n, MeasurableSpace (X n)] {M : ℕ} + +/-- The set of elements of `Σ n : ℕ, X n` with first component at most `M` is measurable. -/ +lemma measurableSet_sigma_fst_le (M : ℕ) : MeasurableSet {x : Σ n, X n | x.1 ≤ M} := + measurable_sigma_fst (MeasurableSet.of_discrete (s := Set.Iic M)) + +/-- The set of elements of `Σ n : ℕ, X n` with first component less than `M` is measurable. -/ +lemma measurableSet_sigma_fst_lt (M : ℕ) : MeasurableSet {x : Σ n, X n | x.1 < M} := + measurable_sigma_fst (MeasurableSet.of_discrete (s := Set.Iio M)) + +/-- The image of a measure on `X (M + 1)` by `Sigma.mk (M + 1)` gives measure zero to the elements +of `Σ n : ℕ, X n` with first component at most `M`. -/ +lemma MeasureTheory.Measure.map_sigmaMk_succ_apply_fst_le (μ : Measure (X (M + 1))) : + (μ.map (Sigma.mk (M + 1))) {x : Σ n, X n | x.1 ≤ M} = 0 := by + rw [Measure.map_apply (measurable_sigma_mk (M + 1)) (measurableSet_sigma_fst_le M)] + have : Sigma.mk (M + 1) ⁻¹' {x : Σ n, X n | x.1 ≤ M} = ∅ := by + ext x + simp + rw [this, measure_empty] + +end Nat diff --git a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean index ba613ae2..99a6fd94 100644 --- a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean +++ b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean @@ -407,4 +407,14 @@ lemma HasCondDistrib.restrict_preimage [SFinite μ] [IsSFiniteKernel κ] _ = (μ.map X).restrict s ⊗ₘ κ := Measure.restrict_compProd_prod_univ _ _ hs _ = (μ.restrict (X ⁻¹' s)).map X ⊗ₘ κ := by rw [Measure.restrict_map hX hs] +omit [StandardBorelSpace Ω] [Nonempty Ω] in +/-- A conditional law given `X` is a conditional law given `X` under the restriction of `P` to an +event determined by `X`, that is, measurable for the σ-algebra generated by `X`. -/ +lemma HasCondDistrib.restrict_of_measurableSet_comap [SFinite μ] [IsSFiniteKernel κ] + (hX : Measurable X) (hY : Measurable Y) + (h : HasCondDistrib Y X κ μ) {s : Set α} (hs : MeasurableSet[mβ.comap X] s) : + HasCondDistrib Y X κ (μ.restrict s) := by + obtain ⟨t, ht, rfl⟩ := MeasurableSpace.measurableSet_comap.1 hs + exact h.restrict_preimage hX hY ht + end ProbabilityTheory diff --git a/LeanMachineLearning/ForMathlib/Probability/Kernel/Sigma.lean b/LeanMachineLearning/ForMathlib/Probability/Kernel/Sigma.lean new file mode 100644 index 00000000..373f7b64 --- /dev/null +++ b/LeanMachineLearning/ForMathlib/Probability/Kernel/Sigma.lean @@ -0,0 +1,44 @@ +/- +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 LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Sigma +public import Mathlib.Probability.Kernel.Composition.MapComap + +/-! +# Kernels on a sigma type + +`Kernel.sigma κ` is the kernel on `Σ a, β a` which is `κ a` on the fiber `β a`. +-/ + +@[expose] public section + +open MeasureTheory + +namespace ProbabilityTheory.Kernel + +variable {α γ : Type*} {β : α → Type*} [∀ a, MeasurableSpace (β a)] {mγ : MeasurableSpace γ} + +/-- The kernel on `Σ a, β a` which is `κ a` on the fiber `β a`. -/ +def sigma (κ : (a : α) → Kernel (β a) γ) : Kernel (Σ a, β a) γ where + toFun x := κ x.1 x.2 + measurable' := measurable_sigma_of_measurable_comp_mk fun a ↦ (κ a).measurable + +@[simp] +lemma sigma_apply (κ : (a : α) → Kernel (β a) γ) (x : Σ a, β a) : sigma κ x = κ x.1 x.2 := rfl + +lemma sigma_apply_mk (κ : (a : α) → Kernel (β a) γ) (a : α) (b : β a) : + sigma κ ⟨a, b⟩ = κ a b := rfl + +lemma comap_sigma_mk (κ : (a : α) → Kernel (β a) γ) (a : α) : + (sigma κ).comap (Sigma.mk a) (measurable_sigma_mk a) = κ a := by + ext b : 1 + rw [comap_apply, sigma_apply_mk] + +instance (κ : (a : α) → Kernel (β a) γ) [∀ a, IsMarkovKernel (κ a)] : IsMarkovKernel (sigma κ) := + ⟨fun x ↦ (IsMarkovKernel.isProbabilityMeasure (κ := κ x.1) x.2)⟩ + +end ProbabilityTheory.Kernel diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean index bfd28276..6c09c653 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithm.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean @@ -305,6 +305,18 @@ lemma history_succ (n : ℕ) : · simp [history, step] · simp [history] +/-- If the history of the first `n` rounds has law `μ` and the round at time `n` has conditional +law `κ` given this history, then the history of the first `n + 1` rounds has law the image of +`μ ⊗ₘ κ` by the identification of `Hist 𝓞 𝓐 𝓨 n × Round 𝓞 𝓐 𝓨` with `Hist 𝓞 𝓐 𝓨 (n + 1)`. -/ +lemma hasLaw_history_succ {P : Measure Ω} {n : ℕ} {μ : Measure (Hist 𝓞 𝓐 𝓨 n)} + {κ : Kernel (Hist 𝓞 𝓐 𝓨 n) (Round 𝓞 𝓐 𝓨)} + (hμ : HasLaw (history O A Y n) μ P) (hκ : HasCondDistrib (step O A Y n) (history O A Y n) κ P) : + HasLaw (history O A Y (n + 1)) + ((μ ⊗ₘ κ).map (MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) n).symm) P := by + rw [history_succ] + exact (hasLaw_map (MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) n).symm.measurable.aemeasurable).comp + (hμ.prodMk_of_hasCondDistrib hκ) + /-- An algorithm-environment sequence: a sequence of observations, actions and feedbacks generated by an algorithm interacting with an environment. -/ structure IsAlgEnvSeq diff --git a/LeanMachineLearning/SequentialLearning/Deterministic.lean b/LeanMachineLearning/SequentialLearning/Deterministic.lean index 66784d36..8fa01ae2 100644 --- a/LeanMachineLearning/SequentialLearning/Deterministic.lean +++ b/LeanMachineLearning/SequentialLearning/Deterministic.lean @@ -39,6 +39,8 @@ measurable functions. The initial action is `fun o ↦ nextA 0 (default, o)`. * `detEnvironment obs f hf`: a deterministic environment with observation kernels `obs`, that gives feedback according to the measurable function `f` (with proof of measurability `hf`). +* `fixedDesignAlg x`: the deterministic algorithm that plays the fixed sequence of actions `x`, + whatever the history and the observations (a *fixed design*). -/ @@ -266,6 +268,20 @@ lemma actionZero_detAlgorithm [MeasurableSpace.SeparatesPoints 𝓐] : unfold actionZero rw [nextAction_detAlgorithm] +/-- The deterministic algorithm that plays the fixed sequence of actions `x : ℕ → 𝓐`, whatever +the history and the observations (a *fixed design*). -/ +noncomputable def fixedDesignAlg (x : ℕ → 𝓐) : Algorithm 𝓞 𝓐 𝓨 := + detAlgorithm (fun n _ ↦ x n) fun _ ↦ measurable_const + +@[simp] +lemma fixedDesignAlg_policy (x : ℕ → 𝓐) (n : ℕ) : + (fixedDesignAlg (𝓞 := 𝓞) (𝓨 := 𝓨) x).policy n = + Kernel.deterministic (fun _ ↦ x n) measurable_const := rfl + +instance (x : ℕ → 𝓐) : + IsDeterministicAlg (fixedDesignAlg (m𝓞 := m𝓞) (m𝓐 := m𝓐) (m𝓨 := m𝓨) x) := + inferInstanceAs (IsDeterministicAlg (detAlgorithm _ _)) + /-- A deterministic environment, where the feedback is given by evaluating fixed measurable functions. -/ noncomputable def detEnvironment (obs : (n : ℕ) → Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓞) diff --git a/LeanMachineLearning/SequentialLearning/IdentificationAlg.lean b/LeanMachineLearning/SequentialLearning/IdentificationAlg.lean index 295fe645..3b9c5e5c 100644 --- a/LeanMachineLearning/SequentialLearning/IdentificationAlg.lean +++ b/LeanMachineLearning/SequentialLearning/IdentificationAlg.lean @@ -5,48 +5,58 @@ Authors: Rémy Degenne -/ module +public import LeanMachineLearning.ForMathlib.Probability.Kernel.Sigma public import LeanMachineLearning.SequentialLearning.Deterministic public import LeanMachineLearning.SequentialLearning.StoppedHistory /-! # Identification algorithms: sampling rule, stopping rule, output rule -An *identification algorithm* with outputs in `𝓞` is an LML sampling rule -`alg : Algorithm Unit 𝓐 𝓨` (an algorithm without observations: LML's observation type is `Unit`, -and `𝓞` denotes here the type of *outputs*) together with +An *identification algorithm* `A : IdentAlg 𝓞 𝓐 𝓨 𝓓` with outputs in `𝓓` is a sampling rule +`A.alg : Algorithm 𝓞 𝓐 𝓨` together with -* a *stopping rule*: `stop n h` says that the algorithm stops after `n` rounds when the history - of these rounds is `h : Hist Unit 𝓐 𝓨 n` (each `{h | stop n h}` is measurable); -* an *output rule*: for each `n`, a Markov kernel `output n` from histories of length `n` to `𝓞` - (the distribution of the output when the algorithm stops after `n` rounds). +* a *stopping rule* `A.stopSet`, a measurable set of histories of variable length: the algorithm + stops after `n` rounds if the history of these `n` rounds belongs to `A.stopSet`; +* an *output rule* `A.output`, a Markov kernel from histories of variable length to `𝓓`: the + distribution of the output given the history of the rounds played. A *run* of the algorithm in an environment `env`, on a probability space `(Ω, P)`, consists of -observation, action and feedback processes `O, X, Y` (with `O` trivially `Unit`-valued) forming an -algorithm-environment sequence for `alg` and `env` (LML `IsAlgEnvSeq`) and an output `out : Ω → 𝓞` -whose conditional law given the history at the -stopping time is the output rule (`IdentAlg.IsRun`). The stopping time `IdentAlg.stoppingTime` -is the stopping time `Learning.stoppingTime` of the stopping rule `A.stopSet` (the hitting time, -Mathlib `hittingAfter`, of the stopping rule by the process of histories), a stopping time of -the history filtration, and the history at the stopping time is `Learning.stoppedHist`. - -Examples: best-arm identification (`𝓞 = 𝓐`, output = recommended arm), hypothesis tests -(`𝓞 = Bool`), estimation (`𝓞 = ℝ`). +observation, action and feedback processes `O, X, Y` forming an algorithm-environment sequence +for `A.alg` and `env` (`IsAlgEnvSeq`) and an output `out : Ω → 𝓓` whose conditional law given the +history at the stopping time is the output rule (`IdentAlg.IsRun`). The stopping time +`IdentAlg.stoppingTime A O X Y` is the stopping time `Learning.stoppingTime` of the stopping rule +`A.stopSet` (the hitting time, Mathlib `hittingAfter`, of the stopping rule by the process of +histories), a stopping time of the history filtration, and the history at the stopping time is +`IdentAlg.stoppedHist A O X Y` (`Learning.stoppedHist`). If the algorithm never stops, the history +at the stopping time is by convention the empty history, and the output is then drawn from the +output rule at the empty history. + +The law of the output of a run is determined by `A` and `env`: it is `A.outputMeasure env`, the +law of the output on the canonical probability space of the interaction (`trajMeasure`), see +`IdentAlg.IsRun.hasLaw_output`. Properties of the algorithm are stated in terms of this law: `A` +is *PAC at level `δ`* (`IdentAlg.IsPAC`) for a family of environments `env θ` and a goodness +predicate `good θ` if, for every `θ`, the output in `env θ` is `good θ` with probability at least +`1 - δ`. `IdentAlg.IsPAC.measureReal_good_of_isRun` transfers this bound to any run of `A`. + +Examples: best-arm identification (`𝓓 = 𝓐`, output = recommended arm), hypothesis tests +(`𝓓 = Bool`), estimation (`𝓓 = ℝ`). A *fixed-budget* algorithm is the special case where the stopping rule is "stop after exactly `T` rounds" (`IsFixedBudget A T`; constructor `fixedBudget alg T ρ`); a *fixed-confidence* -algorithm stops adaptively. +algorithm stops adaptively. A *fixed-design* algorithm (`IsFixedDesign A`) is one whose sampling +rule plays a fixed sequence of actions (`fixedDesignAlg x`). ## Main definitions -* `IdentAlg 𝓐 𝓨 𝓞`: the structure. +* `IdentAlg 𝓞 𝓐 𝓨 𝓓`: the structure. * `IdentAlg.stoppingTime A O X Y : Ω → ℕ∞`: the number of rounds played, a hitting time. -* `IdentAlg.stoppedHist A O X Y : Ω → Σ n, Hist Unit 𝓐 𝓨 n`: the history at the stopping time. +* `IdentAlg.stoppedHist A O X Y : Ω → Σ n, Hist 𝓞 𝓐 𝓨 n`: the history at the stopping time. * `IdentAlg.IsRun A env O X Y out P`: `(O, X, Y, out)` is a run of `A` in `env` on `(Ω, P)`. -* `IdentAlg.IsPAC A env good δ`: for every parameter `θ` of the family `env θ` of environments - and every run of `A` in `env θ`, the output is `good θ` with probability at least `1 - δ`. +* `IdentAlg.outputMeasure A env : Measure 𝓓`: the law of the output of `A` in `env`. +* `IdentAlg.IsPAC A env good δ`: for every parameter `θ`, the output of `A` in `env θ` is + `good θ` with probability at least `1 - δ`. * `IdentAlg.IsFixedBudget A T`, `IdentAlg.fixedBudget alg T ρ`: fixed-budget algorithms. -* `fixedDesignAlg x`: the deterministic algorithm playing the sequence `x` whatever the - observations; `IdentAlg.IsFixedDesign A` says that the sampling rule of `A` is of this form. +* `IdentAlg.IsFixedDesign A`: the sampling rule of `A` is `fixedDesignAlg x` for some `x`. Time is `0`-indexed: after `n` rounds the actions `a_0, …, a_{n-1}` have been played. -/ @@ -57,135 +67,170 @@ open MeasureTheory ProbabilityTheory open scoped ENat -universe u - namespace Learning -variable {𝓞 𝓐 𝓨 𝓓 Ω : Type*} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} - {m𝓞 : MeasurableSpace 𝓞} {m𝓓 : MeasurableSpace 𝓓} {mΩ : MeasurableSpace Ω} - --- TODO: move -/-- The deterministic algorithm that plays the fixed sequence `x : ℕ → 𝓐` regardless of the -observations (a *fixed design*). -/ -noncomputable def fixedDesignAlg (x : ℕ → 𝓐) : Algorithm 𝓞 𝓐 𝓨 := - detAlgorithm (fun n _ ↦ x n) fun _ ↦ measurable_const +variable {𝓞 𝓐 𝓨 𝓓 Ω : Type*} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} + {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} {mΩ : MeasurableSpace Ω} -/-- An identification algorithm with outputs in `𝓞`: a sampling rule `alg`, a stopping rule -`stop` (`stop n h`: stop after `n` rounds when their history is `h`) and an output rule `output` -(the distribution of the output given the history of the `n` rounds played), a Markov kernel. -/ +/-- An identification algorithm with outputs in `𝓓`: a sampling rule `alg`, a stopping rule +`stopSet` (the algorithm stops after `n` rounds if the history of these rounds, as a history of +variable length, belongs to `stopSet`) and an output rule `output`, a Markov kernel giving the +distribution of the output given the history of the rounds played. -/ structure IdentAlg (𝓞 𝓐 𝓨 𝓓 : Type*) [MeasurableSpace 𝓞] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace 𝓓] where /-- The sampling rule. -/ alg : Algorithm 𝓞 𝓐 𝓨 - /-- The stopping rule: `stop n h` means that the algorithm stops after `n` rounds when the - history of these rounds is `h`. -/ - stop : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n → Prop + /-- The stopping rule: the algorithm stops after `n` rounds if the history of these rounds + belongs to `stopSet`. -/ + stopSet : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) /-- The stopping rule is measurable. -/ - measurableSet_stop : ∀ n, MeasurableSet {h | stop n h} - /-- The output rule: distribution of the output given the history of the `n` rounds played. -/ - output : (n : ℕ) → Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓓 - /-- The output rules are Markov kernels. -/ - [isMarkovKernel_output : ∀ n, IsMarkovKernel (output n)] + measurableSet_stopSet : MeasurableSet stopSet + /-- The output rule: distribution of the output given the history of the rounds played. -/ + output : Kernel (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) 𝓓 + /-- The output rule is a Markov kernel. -/ + [isMarkovKernel_output : IsMarkovKernel output] namespace IdentAlg variable (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) -instance (n : ℕ) : IsMarkovKernel (A.output n) := A.isMarkovKernel_output n +instance : IsMarkovKernel A.output := A.isMarkovKernel_output /-- The stopping time of `A` on the observation, action and feedback processes `O`, `X`, `Y`: the -number of rounds -played, that is the first `n` such that the stopping rule fires on the history of the first `n` -rounds (`⊤` if it never does). It is the stopping time `Learning.stoppingTime` of the stopping -rule `{h | A.stop h.1 h.2}`. -/ -noncomputable def stoppingTime : Ω → ℕ∞ := Learning.stoppingTime O X Y {h | A.stop h.1 h.2} +number of rounds played, that is the first `n` such that the history of the first `n` rounds +belongs to the stopping rule `A.stopSet` (`⊤` if there is none). -/ +noncomputable def stoppingTime : Ω → ℕ∞ := Learning.stoppingTime O X Y A.stopSet -lemma stoppingTime_def : - A.stoppingTime O X Y = Learning.stoppingTime O X Y {h | A.stop h.1 h.2} := rfl +lemma stoppingTime_def : A.stoppingTime O X Y = Learning.stoppingTime O X Y A.stopSet := rfl -lemma measurableSet_stopSet : MeasurableSet {h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n | A.stop h.1 h.2} := - measurableSet_sigma_iff.2 A.measurableSet_stop - -/-- The stopping time of an identification algorithm is a stopping time of the history -filtration of any algorithm-environment sequence `X`, `Y`. -/ -lemma isStoppingTime_stoppingTime {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} - {P : Measure Ω} [IsFiniteMeasure P] (h : IsAlgEnvSeq O X Y alg env P) : - IsStoppingTime h.filtration (A.stoppingTime O X Y) := - h.isStoppingTime_stoppingTime A.measurableSet_stopSet - -/-- The history of the rounds played by `A`, as a history of variable length (of length `0` if -`A` never stops): the history stopped at `A.stoppingTime O X Y`. -/ +/-- The history of the rounds played by `A`, as a history of variable length: the history stopped +at `A.stoppingTime O X Y` (the empty history if `A` never stops). -/ noncomputable def stoppedHist : Ω → Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n := Learning.stoppedHist O X Y (A.stoppingTime O X Y) lemma stoppedHist_def : A.stoppedHist O X Y = Learning.stoppedHist O X Y (A.stoppingTime O X Y) := rfl -/-- When the stopping time is finite, the history at the stopping time belongs to the stopping -rule. -/ -lemma stoppedHist_mem_stopSet_of_ne_top {ω : Ω} (h : A.stoppingTime O X Y ω ≠ ⊤) : - A.stoppedHist O X Y ω ∈ {h | A.stop h.1 h.2} := - Learning.stoppedHist_mem_of_ne_top h - -/-- The output rule of `A` as a single kernel on histories of variable length. -/ -noncomputable def outputKernel : Kernel (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) 𝓓 where - toFun h := A.output h.1 h.2 - measurable' := measurable_sigma_of_measurable_comp_mk fun n ↦ (A.output n).measurable +/-- The law of the output of `A` in the environment `env`: the output rule applied to the law of +the history at the stopping time. This is the law of the output of any run of `A` in `env` +(`IsRun.hasLaw_output`). -/ +noncomputable def outputMeasure (env : Environment 𝓞 𝓐 𝓨) : Measure 𝓓 := + A.output ∘ₘ stoppedHistMeasure A.alg env A.stopSet -instance : IsMarkovKernel A.outputKernel := - ⟨fun h ↦ (A.isMarkovKernel_output h.1).isProbabilityMeasure h.2⟩ +instance (env : Environment 𝓞 𝓐 𝓨) : IsProbabilityMeasure (A.outputMeasure env) := by + unfold outputMeasure + infer_instance /-- `(O, X, Y, out)` is a *run* of the identification algorithm `A` in the environment `env` on the probability space `(Ω, P)`: the observation, action and feedback processes `O`, `X`, `Y` form an algorithm-environment sequence for the sampling rule `A.alg` and `env`, and the output `out` has -conditional law `A.output` given the history at the stopping time. -/ +conditional law `A.output` given the history at the stopping time (the empty history if `A` +never stops). -/ structure IsRun (env : Environment 𝓞 𝓐 𝓨) (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (out : Ω → 𝓓) (P : Measure Ω) [IsFiniteMeasure P] : Prop where /-- The actions and feedbacks are generated by the sampling rule in the environment. -/ isAlgEnvSeq : IsAlgEnvSeq O X Y A.alg env P /-- The output is drawn from the output rule applied to the history at the stopping time. -/ - hasCondDistrib_output : HasCondDistrib out (A.stoppedHist O X Y) A.outputKernel P + hasCondDistrib_output : HasCondDistrib out (A.stoppedHist O X Y) A.output P /-- `A` is *PAC at level `δ`* for the family of environments `env : Θ → Environment 𝓞 𝓐 𝓨` and -the goodness predicate `good : Θ → 𝓓 → Prop` if, for every `θ` and every run of `A` in `env θ` on -a probability space `(Ω, P)`, the output is `good θ` with probability at least `1 - δ`. -/ +the goodness predicate `good : Θ → 𝓓 → Prop` if, for every `θ`, the output of `A` in `env θ` is +`good θ` with probability at least `1 - δ`. See `IsPAC.measureReal_good_of_isRun` for the +corresponding statement about any run of `A`. -/ def IsPAC {Θ : Type*} (env : Θ → Environment 𝓞 𝓐 𝓨) (good : Θ → 𝓓 → Prop) (δ : ℝ) : Prop := - ∀ θ, ∀ {Ω : Type u} {_mΩ : MeasurableSpace Ω} (P : Measure Ω) [IsProbabilityMeasure P] - (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (out : Ω → 𝓓), - A.IsRun (env θ) O X Y out P → - 1 - δ ≤ P.real {ω | good θ (out ω)} + ∀ θ, 1 - δ ≤ (A.outputMeasure (env θ)).real {d | good θ d} /-- `A` is a *fixed-budget* algorithm with budget `T` if its stopping rule is "stop after exactly `T` rounds". -/ -def IsFixedBudget (T : ℕ) : Prop := A.stop = fun n _ ↦ n = T +def IsFixedBudget (T : ℕ) : Prop := A.stopSet = {h | h.1 = T} + +/-- `A` is a *fixed-design* algorithm if its sampling rule plays a fixed sequence of actions, +whatever the history and the observations. -/ +def IsFixedDesign : Prop := ∃ x : ℕ → 𝓐, A.alg = fixedDesignAlg x + +variable {A O X Y} {env : Environment 𝓞 𝓐 𝓨} {out : Ω → 𝓓} {P : Measure Ω} + +/-- The stopping time of an identification algorithm is a stopping time of the history +filtration of any algorithm-environment sequence `O`, `X`, `Y`. -/ +lemma isStoppingTime_stoppingTime (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) {alg : Algorithm 𝓞 𝓐 𝓨} + [IsFiniteMeasure P] (h : IsAlgEnvSeq O X Y alg env P) : + IsStoppingTime h.filtration (A.stoppingTime O X Y) := + h.isStoppingTime_stoppingTime A.measurableSet_stopSet + +/-- When the stopping time is finite, the history at the stopping time belongs to the stopping +rule. -/ +lemma stoppedHist_mem_stopSet_of_ne_top {ω : Ω} (h : A.stoppingTime O X Y ω ≠ ⊤) : + A.stoppedHist O X Y ω ∈ A.stopSet := + Learning.stoppedHist_mem_of_ne_top h + +/-- The history at the stopping time of any run of `A` in `env` has law +`stoppedHistMeasure A.alg env A.stopSet`. -/ +lemma IsRun.hasLaw_stoppedHist [IsProbabilityMeasure P] (h : A.IsRun env O X Y out P) : + HasLaw (A.stoppedHist O X Y) (stoppedHistMeasure A.alg env A.stopSet) P := + h.isAlgEnvSeq.hasLaw_stoppedHist_stoppingTime A.measurableSet_stopSet + +/-- The output of any run of `A` in `env` has law `A.outputMeasure env`. -/ +lemma IsRun.hasLaw_output [IsProbabilityMeasure P] (h : A.IsRun env O X Y out P) : + HasLaw out (A.outputMeasure env) P := by + have h_comp := h.hasCondDistrib_output.hasLaw_comp + rw [h.hasLaw_stoppedHist.map_eq] at h_comp + exact h_comp + +/-- For a PAC algorithm at level `δ`, the output of any run in `env θ` is `good θ` with +probability at least `1 - δ`. -/ +lemma IsPAC.measureReal_good_of_isRun {Θ : Type*} {env : Θ → Environment 𝓞 𝓐 𝓨} + {good : Θ → 𝓓 → Prop} {δ : ℝ} (hA : A.IsPAC env good δ) {θ : Θ} + (hgood : MeasurableSet {d | good θ d}) [IsProbabilityMeasure P] + (h : A.IsRun (env θ) O X Y out P) : + 1 - δ ≤ P.real {ω | good θ (out ω)} := by + rw [h.hasLaw_output.measureReal_eq hgood] + exact hA θ + +section FixedBudget + +variable [Nonempty 𝓓] (alg : Algorithm 𝓞 𝓐 𝓨) (T : ℕ) (ρ : Kernel (Hist 𝓞 𝓐 𝓨 T) 𝓓) + [IsMarkovKernel ρ] + +/-- The output rule of a fixed-budget algorithm with output kernel `ρ` on histories of length +`T`: `ρ` on histories of length `T`, an arbitrary constant (never used) on other lengths. -/ +noncomputable def fixedBudgetOutput (n : ℕ) : Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓓 := + if h : n = T then ρ.comap (fun x i ↦ x (Fin.cast h.symm i)) (by fun_prop) + else Kernel.const _ (Measure.dirac (Classical.arbitrary 𝓓)) + +instance (n : ℕ) : IsMarkovKernel (fixedBudgetOutput T ρ n) := by + unfold fixedBudgetOutput + by_cases h : n = T <;> simp only [h, ↓reduceDIte] <;> infer_instance + +omit [IsMarkovKernel ρ] in +@[simp] +lemma fixedBudgetOutput_self : fixedBudgetOutput T ρ T = ρ := by + simp only [fixedBudgetOutput, ↓reduceDIte, Fin.cast_eq_self] + ext y u _ + simp /-- The fixed-budget identification algorithm with sampling rule `alg`, budget `T` and output -kernel `ρ` on histories of length `T` (the output rule at other lengths, never used, is an -arbitrary constant). -/ -noncomputable def fixedBudget [Nonempty 𝓓] (alg : Algorithm 𝓞 𝓐 𝓨) (T : ℕ) - (ρ : Kernel (Hist 𝓞 𝓐 𝓨 T) 𝓓) [IsMarkovKernel ρ] : IdentAlg 𝓞 𝓐 𝓨 𝓓 where +kernel `ρ` on histories of length `T`. -/ +noncomputable def fixedBudget : IdentAlg 𝓞 𝓐 𝓨 𝓓 where alg := alg - stop n _ := n = T - measurableSet_stop n := by by_cases h : n = T <;> simp [h] - output n := if h : n = T then ρ.comap (fun x i ↦ x (Fin.cast h.symm i)) (by fun_prop) - else Kernel.const _ (Measure.dirac (Classical.arbitrary 𝓓)) - isMarkovKernel_output n := by - by_cases h : n = T <;> simp only [h, ↓reduceDIte] <;> infer_instance - -lemma isFixedBudget_fixedBudget [Nonempty 𝓞] (alg : Algorithm Unit 𝓐 𝓨) (T : ℕ) - (ρ : Kernel (Hist Unit 𝓐 𝓨 T) 𝓞) [IsMarkovKernel ρ] : - (fixedBudget alg T ρ).IsFixedBudget T := rfl - -/-- The output rule of `fixedBudget alg T ρ` at the budget `T` is `ρ`. -/ -lemma output_fixedBudget [Nonempty 𝓞] (alg : Algorithm Unit 𝓐 𝓨) (T : ℕ) - (ρ : Kernel (Hist Unit 𝓐 𝓨 T) 𝓞) [IsMarkovKernel ρ] : - (fixedBudget alg T ρ).output T = ρ := by - change (if h : T = T then ρ.comap (fun x i ↦ x (Fin.cast h.symm i)) (by fun_prop) - else Kernel.const _ (Measure.dirac (Classical.arbitrary 𝓞))) = ρ - simp only [↓reduceDIte, Fin.cast_eq_self] - ext y u _ + stopSet := {h | h.1 = T} + measurableSet_stopSet := measurable_sigma_fst (MeasurableSet.of_discrete (s := {T})) + output := Kernel.sigma (fixedBudgetOutput T ρ) + +@[simp] lemma alg_fixedBudget : (fixedBudget alg T ρ).alg = alg := rfl + +@[simp] lemma stopSet_fixedBudget : (fixedBudget alg T ρ).stopSet = {h | h.1 = T} := rfl + +@[simp] lemma output_fixedBudget : + (fixedBudget alg T ρ).output = Kernel.sigma (fixedBudgetOutput T ρ) := rfl + +lemma isFixedBudget_fixedBudget : (fixedBudget alg T ρ).IsFixedBudget T := rfl + +/-- The output rule of `fixedBudget alg T ρ` on a history of length `T` is `ρ`. -/ +lemma output_fixedBudget_mk (h : Hist 𝓞 𝓐 𝓨 T) : (fixedBudget alg T ρ).output ⟨T, h⟩ = ρ h := by simp +end FixedBudget + end IdentAlg end Learning diff --git a/LeanMachineLearning/SequentialLearning/StoppedHistory.lean b/LeanMachineLearning/SequentialLearning/StoppedHistory.lean index e098c529..ff4be271 100644 --- a/LeanMachineLearning/SequentialLearning/StoppedHistory.lean +++ b/LeanMachineLearning/SequentialLearning/StoppedHistory.lean @@ -7,7 +7,7 @@ module public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Sigma public import LeanMachineLearning.ForMathlib.Probability.HasLaw -public import LeanMachineLearning.SequentialLearning.Algorithm +public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace public import Mathlib.Probability.Process.HittingTime /-! @@ -16,29 +16,30 @@ public import Mathlib.Probability.Process.HittingTime A *stopping rule* is a measurable set `S : Set (Σ n, Hist 𝓞 𝓐 𝓨 n)` of histories of variable length: the interaction stops after `n` rounds if the history of these `n` rounds belongs to `S`. Its *stopping time* `stoppingTime O X Y S : Ω → ℕ∞` is the number of rounds played, the -hitting time (Mathlib `hittingAfter`) of `S` by the process `n ↦ ⟨n, history O X Y n⟩`. For a -random time `τ : Ω → ℕ∞`, `stoppedHist O X Y τ` is the history of the first `τ` rounds, as a -history of variable length (of length `0` if `τ = ⊤`). +hitting time (Mathlib `hittingAfter`) of `S` by the process `sigmaHistory O X Y` of the histories +seen as histories of variable length. For a random time `τ : Ω → ℕ∞`, `stoppedHist O X Y τ` is +the history of the first `τ` rounds, as a history of variable length: it is the stopped value +(Mathlib `stoppedValue`) of the process `sigmaHistory O X Y` at `τ`, except that when `τ = ⊤` it +is the empty history rather than an arbitrary value. * `stoppingTime_le_iff`, `lt_stoppingTime_iff`, `stoppingTime_eq_coe_iff`, `stoppingTime_eq_top_iff`: characterizations of the stopping time; * `stoppedHist_mem_of_ne_top`: the stopped history belongs to `S` when the stopping time is finite; `notMem_of_lt_stoppingTime`: the history of `n < τ` rounds does not; * `measurable_stoppingTime`, `measurable_stoppedHist`; -* `IsAlgEnvSeq.isStoppingTime_stoppingTime`: `stoppingTime O X Y S` is a stopping time of the - history filtration of an algorithm-environment sequence; -* `exists_measurableSet_preimage_lt_stoppingTime`: the event `{n < stoppingTime O X Y S}` is - determined by the first `n` rounds; +* `measurableSet_comap_history_lt_stoppingTime`, `measurableSet_comap_history_stoppingTime_le`: + the events `{n < stoppingTime O X Y S}` and `{stoppingTime O X Y S ≤ n}` are determined by the + first `n` rounds; `IsAlgEnvSeq.isStoppingTime_stoppingTime`: `stoppingTime O X Y S` is a + stopping time of the history filtration of an algorithm-environment sequence; * `hasLaw_stoppedHist_min_add`, `hasLaw_stoppedHist_min_succ_add`: the laws of the histories stopped at `min τ M` and `min τ (M + 1)` split according to whether `τ ≤ M`; - `IsAlgEnvSeq.hasCondDistrib_step_restrict_lt_stoppingTime`, - `IsAlgEnvSeq.hasCondDistrib_obs_restrict_lt_stoppingTime`, - `IsAlgEnvSeq.hasCondDistrib_action_restrict_lt_stoppingTime`: on the event `{M < τ}`, which is - determined by the first `M` rounds, the step, the observation and the action at round `M` keep - their conditional laws; `IsAlgEnvSeq.hasLaw_history_succ_restrict_lt_stoppingTime`: on this +* `IsAlgEnvSeq.hasCondDistrib_step_restrict_lt_stoppingTime` (and `obs`, `action`, `feedback`): + on the event `{M < τ}`, which is determined by the first `M` rounds, the round at time `M` keeps + its conditional laws; `IsAlgEnvSeq.hasLaw_history_succ_restrict_lt_stoppingTime`: on this event, the law of the first `M + 1` rounds is the composition-product of the law of the first - `M` rounds with the step kernel. - + `M` rounds with the step kernel; +* `stoppedHistMeasure alg env S`, `IsAlgEnvSeq.hasLaw_stoppedHist_stoppingTime`: the law of the + history stopped by `S` is determined by the algorithm and the environment. -/ @[expose] public section @@ -51,49 +52,57 @@ namespace Learning variable {𝓞 𝓐 𝓨 Ω : Type*} {mΩ : MeasurableSpace Ω} -/-- The stopping time of the stopping rule `S` on the action and feedback processes `X`, `Y`: -the number of rounds played, that is the first `n` such that the history of the first `n` rounds -belongs to `S` (`⊤` if there is none). -/ +/-- The history of the first `n` rounds, as a history of variable length: the process +`n ↦ ⟨n, history O X Y n⟩`, of which the stopping time of a stopping rule is a hitting time. -/ +def sigmaHistory (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) : + Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n := + ⟨n, history O X Y n ω⟩ + +/-- The stopping time of the stopping rule `S` on the observation, action and feedback processes +`O`, `X`, `Y`: the number of rounds played, that is the first `n` such that the history of the +first `n` rounds belongs to `S` (`⊤` if there is none). -/ noncomputable def stoppingTime (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) : Ω → ℕ∞ := - hittingAfter (fun n ω ↦ (⟨n, history O X Y n ω⟩ : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) S 0 + hittingAfter (sigmaHistory O X Y) S 0 -/-- The history of the first `τ ω` rounds, as a history of variable length (of length `0` if -`τ ω = ⊤`). -/ +/-- The history of the first `τ ω` rounds, as a history of variable length. When `τ ω = ⊤`, this +is the empty history (Mathlib's `stoppedValue` would use an arbitrary value instead). -/ noncomputable def stoppedHist (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (τ : Ω → ℕ∞) (ω : Ω) : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n := - ⟨(τ ω).toNat, history O X Y _ ω⟩ + sigmaHistory O X Y (τ ω).toNat ω variable {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} {τ : Ω → ℕ∞} {ω : Ω} {n M : ℕ} +lemma sigmaHistory_apply (n : ℕ) (ω : Ω) : + sigmaHistory O X Y n ω = ⟨n, history O X Y n ω⟩ := rfl + +lemma fst_sigmaHistory (n : ℕ) (ω : Ω) : (sigmaHistory O X Y n ω).1 = n := rfl + section stoppingTime lemma stoppingTime_le_iff : - stoppingTime O X Y S ω ≤ n ↔ ∃ j ≤ n, (⟨j, history O X Y j ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∈ S := - (hittingAfter_le_iff (u := fun n ω ↦ (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n)) - (s := S) (n := 0) (i := n) (ω := ω)).trans (by simp) + stoppingTime O X Y S ω ≤ n ↔ ∃ j ≤ n, sigmaHistory O X Y j ω ∈ S := + (hittingAfter_le_iff (u := sigmaHistory O X Y) (s := S) (n := 0) (i := n) (ω := ω)).trans + (by simp) lemma lt_stoppingTime_iff : - (n : ℕ∞) < stoppingTime O X Y S ω ↔ - ∀ j ≤ n, (⟨j, history O X Y j ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∉ S := by + (n : ℕ∞) < stoppingTime O X Y S ω ↔ ∀ j ≤ n, sigmaHistory O X Y j ω ∉ S := by rw [← not_le, stoppingTime_le_iff] simp lemma stoppingTime_eq_top_iff : - stoppingTime O X Y S ω = ⊤ ↔ ∀ n, (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∉ S := - (hittingAfter_eq_top_iff (u := fun n ω ↦ (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n)) - (s := S) (n := 0) (ω := ω)).trans (by simp) + stoppingTime O X Y S ω = ⊤ ↔ ∀ n, sigmaHistory O X Y n ω ∉ S := + (hittingAfter_eq_top_iff (u := sigmaHistory O X Y) (s := S) (n := 0) (ω := ω)).trans (by simp) lemma notMem_of_lt_stoppingTime (h : (n : ℕ∞) < stoppingTime O X Y S ω) : - (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∉ S := + sigmaHistory O X Y n ω ∉ S := notMem_of_lt_hittingAfter h (Nat.zero_le n) lemma stoppingTime_eq_coe_iff : stoppingTime O X Y S ω = n ↔ - (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∈ S ∧ - ∀ j < n, (⟨j, history O X Y j ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∉ S := by + sigmaHistory O X Y n ω ∈ S ∧ ∀ j < n, sigmaHistory O X Y j ω ∉ S := by constructor · intro h refine ⟨?_, fun j hj ↦ notMem_of_lt_stoppingTime (h ▸ ENat.natCast_lt_natCast.2 hj)⟩ @@ -116,8 +125,8 @@ lemma stoppedHist_congr (τ τ' : Ω → ℕ∞) (h : τ ω = τ' ω) : rw [h] lemma stoppedHist_coe (M : ℕ) (ω : Ω) : - stoppedHist O X Y (fun _ ↦ (M : ℕ∞)) ω = ⟨M, history O X Y M ω⟩ := by - change (⟨(M : ℕ∞).toNat, history O X Y (M : ℕ∞).toNat ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) = _ + stoppedHist O X Y (fun _ ↦ (M : ℕ∞)) ω = sigmaHistory O X Y M ω := by + change sigmaHistory O X Y (M : ℕ∞).toNat ω = _ rw [ENat.toNat_natCast] /-- The stopped history belongs to the stopping rule when the stopping time is finite. -/ @@ -134,14 +143,14 @@ lemma stoppedHist_min_of_le (h : τ ω ≤ M) : /-- If `M < τ ω`, the history stopped at `min τ M` is the history of the first `M` rounds. -/ lemma stoppedHist_min_of_lt (h : (M : ℕ∞) < τ ω) : - stoppedHist O X Y (fun ω ↦ min (τ ω) M) ω = ⟨M, history O X Y M ω⟩ := by + stoppedHist O X Y (fun ω ↦ min (τ ω) M) ω = sigmaHistory O X Y M ω := by rw [stoppedHist_congr (fun ω ↦ min (τ ω) M) (fun _ ↦ (M : ℕ∞)) (min_eq_right h.le), stoppedHist_coe] /-- If `M < τ ω`, the history stopped at `min τ (M + 1)` is the history of the first `M + 1` rounds. -/ lemma stoppedHist_min_succ_of_lt (h : (M : ℕ∞) < τ ω) : - stoppedHist O X Y (fun ω ↦ min (τ ω) (M + 1 : ℕ)) ω = ⟨M + 1, history O X Y (M + 1) ω⟩ := by + stoppedHist O X Y (fun ω ↦ min (τ ω) (M + 1 : ℕ)) ω = sigmaHistory O X Y (M + 1) ω := by rw [stoppedHist_congr (fun ω ↦ min (τ ω) (M + 1 : ℕ)) (fun _ ↦ ((M + 1 : ℕ) : ℕ∞)) (min_eq_right ?_), stoppedHist_coe] exact_mod_cast Order.add_one_le_of_lt h @@ -160,6 +169,24 @@ lemma stoppedHist_min_zero (τ : Ω → ℕ∞) : end stoppingTime +section natCast + +omit mΩ in +lemma compl_setOf_le_natCast (τ : Ω → ℕ∞) (M : ℕ) : + {ω | τ ω ≤ M}ᶜ = {ω | (M : ℕ∞) < τ ω} := by + ext ω + simp + +/-- Every subset of `ℕ∞` is measurable, hence so is `{τ ≤ M}` for a measurable `τ`. -/ +lemma measurableSet_le_natCast (hτ : Measurable τ) (M : ℕ) : MeasurableSet {ω | τ ω ≤ M} := + hτ (MeasurableSet.of_discrete (s := Set.Iic (M : ℕ∞))) + +lemma measurableSet_natCast_lt (hτ : Measurable τ) (M : ℕ) : + MeasurableSet {ω | (M : ℕ∞) < τ ω} := + hτ (MeasurableSet.of_discrete (s := Set.Ioi (M : ℕ∞))) + +end natCast + variable {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} /-- The history stopped at `min τ 0` has law the Dirac mass at the empty history. -/ @@ -169,132 +196,118 @@ lemma hasLaw_stoppedHist_min_zero (P : Measure Ω) [IsProbabilityMeasure P] (τ rw [stoppedHist_min_zero] exact hasLaw_dirac_of_ae_eq (ae_eq_refl _) -section measurableSet - -/-- The set of histories of variable length of length at most `M` is measurable. -/ -lemma measurableSet_fst_le (M : ℕ) : - MeasurableSet {h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n | h.1 ≤ M} := - measurable_sigma_fst (MeasurableSet.of_discrete (s := Set.Iic M)) - -/-- The set of histories of variable length of length less than `M` is measurable. -/ -lemma measurableSet_fst_lt (M : ℕ) : - MeasurableSet {h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n | h.1 < M} := - measurable_sigma_fst (MeasurableSet.of_discrete (s := Set.Iio M)) - -omit m𝓞 m𝓐 m𝓨 in -lemma measurable_min_natCast (hτ : Measurable τ) (M : ℕ) : - Measurable fun ω ↦ min (τ ω) (M : ℕ∞) := - (measurable_from_top (f := fun t : ℕ∞ ↦ min t M)).comp hτ - -end measurableSet - section measurability variable (hO : ∀ n, Measurable (O n)) (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n)) include hO hX hY +lemma measurable_sigmaHistory (n : ℕ) : Measurable (sigmaHistory O X Y n) := + (measurable_sigma_mk n).comp (measurable_history hO hX hY n) + lemma measurable_stoppingTime (hS : MeasurableSet S) : Measurable (stoppingTime O X Y S) := by - have hu : ∀ n, Measurable fun ω ↦ (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) := - fun n ↦ (measurable_sigma_mk n).comp (measurable_history hO hX hY n) refine measurable_to_countable' fun x ↦ ?_ induction x using ENat.recTopCoe with | top => - have : stoppingTime O X Y S ⁻¹' {⊤} = - ⋂ n, (fun ω ↦ (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n)) ⁻¹' Sᶜ := by + have : stoppingTime O X Y S ⁻¹' {⊤} = ⋂ n, sigmaHistory O X Y n ⁻¹' Sᶜ := by ext ω simp [stoppingTime_eq_top_iff] rw [this] - exact MeasurableSet.iInter fun n ↦ hu n hS.compl + exact MeasurableSet.iInter fun n ↦ measurable_sigmaHistory hO hX hY n hS.compl | coe n => have : stoppingTime O X Y S ⁻¹' {(n : ℕ∞)} = - (fun ω ↦ (⟨n, history O X Y n ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n)) ⁻¹' S ∩ - ⋂ j < n, (fun ω ↦ (⟨j, history O X Y j ω⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n)) ⁻¹' Sᶜ := by + sigmaHistory O X Y n ⁻¹' S ∩ ⋂ j < n, sigmaHistory O X Y j ⁻¹' Sᶜ := by ext ω simp [stoppingTime_eq_coe_iff] rw [this] - exact (hu n hS).inter (MeasurableSet.biInter (Set.to_countable _) fun j _ ↦ hu j hS.compl) - -lemma measurableSet_stoppingTime_le (hS : MeasurableSet S) (M : ℕ) : - MeasurableSet {ω | stoppingTime O X Y S ω ≤ M} := - measurable_stoppingTime hO hX hY hS (MeasurableSet.of_discrete (s := Set.Iic (M : ℕ∞))) - -lemma measurableSet_lt_stoppingTime (hS : MeasurableSet S) (M : ℕ) : - MeasurableSet {ω | (M : ℕ∞) < stoppingTime O X Y S ω} := - measurable_stoppingTime hO hX hY hS (MeasurableSet.of_discrete (s := Set.Ioi (M : ℕ∞))) + exact (measurable_sigmaHistory hO hX hY n hS).inter + (MeasurableSet.biInter (Set.to_countable _) fun j _ ↦ + measurable_sigmaHistory hO hX hY j hS.compl) lemma measurable_stoppedHist (hτ : Measurable τ) : Measurable (stoppedHist O X Y τ) := Measurable.sigmaMk (measurable_from_top.comp hτ) (measurable_history hO hX hY) lemma measurable_stoppedHist_min (hτ : Measurable τ) (M : ℕ) : Measurable (stoppedHist O X Y fun ω ↦ min (τ ω) M) := - measurable_stoppedHist hO hX hY (measurable_min_natCast hτ M) - -omit hO hX hY in -/-- The event `{n < stoppingTime O X Y S}` is determined by the history of the first `n` rounds. -/ -lemma exists_measurableSet_preimage_lt_stoppingTime (hS : MeasurableSet S) (n : ℕ) : - ∃ B : Set (Hist 𝓞 𝓐 𝓨 n), MeasurableSet B ∧ - {ω | (n : ℕ∞) < stoppingTime O X Y S ω} = history O X Y n ⁻¹' B := by - refine ⟨⋂ j, ⋂ (hj : j ≤ n), + measurable_stoppedHist hO hX hY ((measurable_from_top (f := fun t : ℕ∞ ↦ min t M)).comp hτ) + +end measurability + +section comap + +/-- The event `{n < stoppingTime O X Y S}` is determined by the history of the first `n` rounds: +it is measurable for the σ-algebra generated by `history O X Y n`. -/ +lemma measurableSet_comap_history_lt_stoppingTime (hS : MeasurableSet S) (n : ℕ) : + MeasurableSet[MeasurableSpace.comap (history O X Y n) inferInstance] + {ω | (n : ℕ∞) < stoppingTime O X Y S ω} := by + refine MeasurableSpace.measurableSet_comap.2 ⟨⋂ j, ⋂ (hj : j ≤ n), {h | (⟨j, fun i ↦ h (Fin.castLE hj i)⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∉ S}, ?_, ?_⟩ · refine MeasurableSet.iInter fun j ↦ MeasurableSet.iInter fun hj ↦ ?_ exact ((measurable_sigma_mk j).comp (Measurable.of_eval fun _ ↦ measurable_pi_apply _)) hS.compl · ext ω - simp only [Set.mem_ofPred_eq, lt_stoppingTime_iff, Set.mem_preimage, Set.mem_iInter] + simp only [Set.mem_preimage, Set.mem_iInter, Set.mem_ofPred_eq, lt_stoppingTime_iff] exact ⟨fun h j hj ↦ h j hj, fun h j hj ↦ h j hj⟩ -end measurability +/-- The event `{stoppingTime O X Y S ≤ n}` is determined by the history of the first `n` +rounds: it is measurable for the σ-algebra generated by `history O X Y n`. -/ +lemma measurableSet_comap_history_stoppingTime_le (hS : MeasurableSet S) (n : ℕ) : + MeasurableSet[MeasurableSpace.comap (history O X Y n) inferInstance] + {ω | stoppingTime O X Y S ω ≤ n} := by + rw [← compl_compl {ω | stoppingTime O X Y S ω ≤ n}, compl_setOf_le_natCast] + exact (measurableSet_comap_history_lt_stoppingTime hS n).compl -section law +end comap -variable (hO : ∀ n, Measurable (O n)) (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n)) - (hS : MeasurableSet S) {P : Measure Ω} -include hO hX hY hS +section law -omit m𝓞 m𝓐 m𝓨 hO hX hY hS in -lemma compl_setOf_stoppingTime_le : - {ω | stoppingTime O X Y S ω ≤ M}ᶜ = {ω | (M : ℕ∞) < stoppingTime O X Y S ω} := by - ext ω - simp +variable {P : Measure Ω} /-- The law of the history stopped at `min τ M` splits according to whether `τ ≤ M`: on `{τ ≤ M}` it is the law of the history stopped at `τ` (or equivalently at `min τ M`), on `{M < τ}` it is the law of the history of the first `M` rounds. -/ -lemma hasLaw_stoppedHist_min_add {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} +lemma hasLaw_stoppedHist_min_add (hτ : Measurable τ) {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} {ν : Measure (Hist 𝓞 𝓐 𝓨 M)} - (hμ : HasLaw (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M) μ - (P.restrict {ω | stoppingTime O X Y S ω ≤ M})) - (hν : HasLaw (history O X Y M) ν (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω})) : - HasLaw (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M) - (μ + ν.map (Sigma.mk M)) P := by - refine hμ.add_of_restrict_compl (measurableSet_stoppingTime_le hO hX hY hS M) ?_ - rw [compl_setOf_stoppingTime_le] + (hμ : HasLaw (stoppedHist O X Y fun ω ↦ min (τ ω) M) μ (P.restrict {ω | τ ω ≤ M})) + (hν : HasLaw (history O X Y M) ν (P.restrict {ω | (M : ℕ∞) < τ ω})) : + HasLaw (stoppedHist O X Y fun ω ↦ min (τ ω) M) (μ + ν.map (Sigma.mk M)) P := by + refine hμ.add_of_restrict_compl (measurableSet_le_natCast hτ M) ?_ + rw [compl_setOf_le_natCast] refine (((measurable_sigma_mk M).hasLaw_map ν).comp hν).congr - ((ae_restrict_iff' (measurableSet_lt_stoppingTime hO hX hY hS M)).2 + ((ae_restrict_iff' (measurableSet_natCast_lt hτ M)).2 (Filter.Eventually.of_forall fun ω hω ↦ ?_)) exact stoppedHist_min_of_lt hω /-- The law of the history stopped at `min τ (M + 1)` splits according to whether `τ ≤ M`: on `{τ ≤ M}` it is the law of the history stopped at `min τ M`, on `{M < τ}` it is the law of the history of the first `M + 1` rounds. -/ -lemma hasLaw_stoppedHist_min_succ_add {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} - {ν : Measure (Hist 𝓞 𝓐 𝓨 (M + 1))} - (hμ : HasLaw (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M) μ - (P.restrict {ω | stoppingTime O X Y S ω ≤ M})) - (hν : HasLaw (history O X Y (M + 1)) ν - (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω})) : - HasLaw (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) (M + 1 : ℕ)) - (μ + ν.map (Sigma.mk (M + 1))) P := by - refine HasLaw.add_of_restrict_compl (measurableSet_stoppingTime_le hO hX hY hS M) ?_ ?_ - · refine hμ.congr ((ae_restrict_iff' (measurableSet_stoppingTime_le hO hX hY hS M)).2 +lemma hasLaw_stoppedHist_min_succ_add (hτ : Measurable τ) + {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} {ν : Measure (Hist 𝓞 𝓐 𝓨 (M + 1))} + (hμ : HasLaw (stoppedHist O X Y fun ω ↦ min (τ ω) M) μ (P.restrict {ω | τ ω ≤ M})) + (hν : HasLaw (history O X Y (M + 1)) ν (P.restrict {ω | (M : ℕ∞) < τ ω})) : + HasLaw (stoppedHist O X Y fun ω ↦ min (τ ω) (M + 1 : ℕ)) (μ + ν.map (Sigma.mk (M + 1))) P := by + refine HasLaw.add_of_restrict_compl (measurableSet_le_natCast hτ M) ?_ ?_ + · refine hμ.congr ((ae_restrict_iff' (measurableSet_le_natCast hτ M)).2 (Filter.Eventually.of_forall fun ω hω ↦ ?_)) rw [stoppedHist_min_of_le hω, stoppedHist_min_of_le (hω.trans (by exact_mod_cast M.le_succ))] - · rw [compl_setOf_stoppingTime_le] + · rw [compl_setOf_le_natCast] refine (((measurable_sigma_mk (M + 1)).hasLaw_map ν).comp hν).congr - ((ae_restrict_iff' (measurableSet_lt_stoppingTime hO hX hY hS M)).2 + ((ae_restrict_iff' (measurableSet_natCast_lt hτ M)).2 (Filter.Eventually.of_forall fun ω hω ↦ ?_)) exact stoppedHist_min_succ_of_lt hω +/-- The history stopped at `min τ M` has length at most `M`: its law gives measure zero to the +histories of length `> M`. -/ +lemma _root_.ProbabilityTheory.HasLaw.stoppedHist_min_apply_compl_fst_le + {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} + (hμ : HasLaw (stoppedHist O X Y fun ω ↦ min (τ ω) M) μ P) : + μ {h | h.1 ≤ M}ᶜ = 0 := + hμ.measure_eq_zero_of_ae_notMem (measurableSet_sigma_fst_le M).compl + (ae_of_all _ fun _ h ↦ h fst_stoppedHist_min_le) + +variable (hO : ∀ n, Measurable (O n)) (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n)) + (hS : MeasurableSet S) +include hO hX hY hS + /-- On `{τ ≤ M}`, the history stopped at `min τ M` belongs to the stopping rule: its law under the restriction of `P` to `{τ ≤ M}` gives measure zero to `Sᶜ`. -/ lemma _root_.ProbabilityTheory.HasLaw.stoppedHist_min_restrict_stoppingTime_le_apply_compl @@ -303,21 +316,11 @@ lemma _root_.ProbabilityTheory.HasLaw.stoppedHist_min_restrict_stoppingTime_le_a (P.restrict {ω | stoppingTime O X Y S ω ≤ M})) : μ Sᶜ = 0 := by refine hμ.measure_eq_zero_of_ae_notMem hS.compl - ((ae_restrict_iff' (measurableSet_stoppingTime_le hO hX hY hS M)).2 + ((ae_restrict_iff' (measurableSet_le_natCast (measurable_stoppingTime hO hX hY hS) M)).2 (Filter.Eventually.of_forall fun ω hω h ↦ h ?_)) rw [stoppedHist_min_of_le hω] exact stoppedHist_mem_of_ne_top (ne_top_of_le_ne_top (ENat.natCast_ne_top M) hω) -omit hO hX hY hS in -/-- The history stopped at `min τ M` has length at most `M`: its law gives measure zero to the -histories of length `> M`. -/ -lemma _root_.ProbabilityTheory.HasLaw.stoppedHist_min_apply_compl_fst_le - {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} - (hμ : HasLaw (stoppedHist O X Y fun ω ↦ min (τ ω) M) μ P) : - μ {h | h.1 ≤ M}ᶜ = 0 := - hμ.measure_eq_zero_of_ae_notMem (measurableSet_fst_le M).compl - (ae_of_all _ fun _ h ↦ h fst_stoppedHist_min_le) - /-- On `{M < τ}`, the history of the first `M` rounds does not belong to the stopping rule: if it has law `ν` under the restriction of `P` to `{M < τ}`, the image of `ν` by `Sigma.mk M` gives measure zero to `S`. -/ @@ -326,19 +329,9 @@ lemma _root_.ProbabilityTheory.HasLaw.history_restrict_lt_stoppingTime_map_sigma (hν : HasLaw (history O X Y M) ν (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω})) : (ν.map (Sigma.mk M)) S = 0 := (((measurable_sigma_mk M).hasLaw_map ν).comp hν).measure_eq_zero_of_ae_notMem hS - ((ae_restrict_iff' (measurableSet_lt_stoppingTime hO hX hY hS M)).2 + ((ae_restrict_iff' (measurableSet_natCast_lt (measurable_stoppingTime hO hX hY hS) M)).2 (Filter.Eventually.of_forall fun _ hω ↦ notMem_of_lt_stoppingTime hω)) -omit hO hX hY hS in -/-- A history of length `M + 1` does not have length at most `M`. -/ -lemma map_sigmaMk_succ_apply_fst_le (μ : Measure (Hist 𝓞 𝓐 𝓨 (M + 1))) : - (μ.map (Sigma.mk (M + 1))) {h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n | h.1 ≤ M} = 0 := by - rw [Measure.map_apply (measurable_sigma_mk (M + 1)) (measurableSet_fst_le M)] - have : Sigma.mk (M + 1) ⁻¹' {h : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n | h.1 ≤ M} = ∅ := by - ext h - simp - rw [this, measure_empty] - end law section filtration @@ -346,8 +339,7 @@ section filtration variable {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : Measure Ω} [IsFiniteMeasure P] lemma IsAlgEnvSeq.adapted_sigmaHistory (h : IsAlgEnvSeq O X Y alg env P) : - Adapted h.filtration - (fun n ω ↦ (⟨n, history O X Y n ω⟩ : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) := + Adapted h.filtration (sigmaHistory O X Y) := fun n ↦ (measurable_sigma_mk n).comp (h.adapted_history n) /-- The stopping time of a stopping rule is a stopping time of the history filtration of any @@ -357,57 +349,104 @@ lemma IsAlgEnvSeq.isStoppingTime_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) IsStoppingTime h.filtration (stoppingTime O X Y S) := h.adapted_sigmaHistory.isStoppingTime_hittingAfter hS -/-- On the event `{M < τ}`, which is determined by the first `M` rounds, the step at round `M` +/-- On the event `{M < τ}`, which is determined by the first `M` rounds, the round at time `M` keeps its conditional law given the first `M` rounds. -/ lemma IsAlgEnvSeq.hasCondDistrib_step_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) (hS : MeasurableSet S) (M : ℕ) : HasCondDistrib (step O X Y M) (history O X Y M) (stepKernel alg env M) - (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) := by - obtain ⟨B, hB, hB_eq⟩ := - exists_measurableSet_preimage_lt_stoppingTime (O := O) (X := X) (Y := Y) hS M - rw [hB_eq] - exact (h.hasCondDistrib_step M).restrict_preimage - (h.measurable_history M) (h.measurable_step M) hB + (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) := + (h.hasCondDistrib_step M).restrict_of_measurableSet_comap (h.measurable_history M) + (h.measurable_step M) (measurableSet_comap_history_lt_stoppingTime hS M) -/-- On the event `{M < τ}`, if the first `M` rounds have law `μ`, the first `M + 1` rounds have -law the composition-product of `μ` with the step kernel. -/ -lemma IsAlgEnvSeq.hasLaw_history_succ_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) - (hS : MeasurableSet S) {μ : Measure (Hist 𝓞 𝓐 𝓨 M)} - (hμ : HasLaw (history O X Y M) μ (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω})) : - HasLaw (history O X Y (M + 1)) - ((μ ⊗ₘ stepKernel alg env M).map (MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) M).symm) - (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) := by - rw [history_succ] - exact ((MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) M).symm.measurable.hasLaw_map _).comp - (hμ.prodMk_of_hasCondDistrib (h.hasCondDistrib_step_restrict_lt_stoppingTime hS M)) - -/-- On the event `{M < τ}`, which is determined by the first `M` rounds, the observation at round +/-- On the event `{M < τ}`, which is determined by the first `M` rounds, the observation at time `M` keeps its conditional law given the first `M` rounds. -/ lemma IsAlgEnvSeq.hasCondDistrib_obs_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) (hS : MeasurableSet S) (M : ℕ) : HasCondDistrib (O M) (history O X Y M) (env.obs M) - (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) := by - obtain ⟨B, hB, hB_eq⟩ := - exists_measurableSet_preimage_lt_stoppingTime (O := O) (X := X) (Y := Y) hS M - rw [hB_eq] - exact (h.hasCondDistrib_obs M).restrict_preimage (h.measurable_history M) (h.measurable_obs M) hB - -/-- On the event `{M < τ}`, which is determined by the first `M` rounds, the action at round `M` -keeps its conditional law given the first `M` rounds and the observation at round `M`. -/ + (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) := + (h.hasCondDistrib_obs M).restrict_of_measurableSet_comap (h.measurable_history M) + (h.measurable_obs M) (measurableSet_comap_history_lt_stoppingTime hS M) + +/-- On the event `{M < τ}`, which is determined by the first `M` rounds, the action at time `M` +keeps its conditional law given the first `M` rounds and the observation at time `M`. -/ lemma IsAlgEnvSeq.hasCondDistrib_action_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) (hS : MeasurableSet S) (M : ℕ) : HasCondDistrib (X M) (fun ω ↦ (history O X Y M ω, O M ω)) (alg.policy M) - (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) := by - obtain ⟨B, hB, hB_eq⟩ := - exists_measurableSet_preimage_lt_stoppingTime (O := O) (X := X) (Y := Y) hS M - have hB' : history O X Y M ⁻¹' B = (fun ω ↦ (history O X Y M ω, O M ω)) ⁻¹' (B ×ˢ Set.univ) := by - ext ω - simp - rw [hB_eq, hB'] - exact (h.hasCondDistrib_action M).restrict_preimage + (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) := + (h.hasCondDistrib_action M).restrict_of_measurableSet_comap ((h.measurable_history M).prodMk (h.measurable_obs M)) (h.measurable_action M) - (hB.prod MeasurableSet.univ) + (measurable_iff_comap_le.mp (h.measurable_history_filtrationObs M) _ + (measurableSet_comap_history_lt_stoppingTime hS M)) + +/-- On the event `{M < τ}`, which is determined by the first `M` rounds, the feedback at time `M` +keeps its conditional law given the first `M` rounds, the observation and the action at time +`M`. -/ +lemma IsAlgEnvSeq.hasCondDistrib_feedback_restrict_lt_stoppingTime + (h : IsAlgEnvSeq O X Y alg env P) (hS : MeasurableSet S) (M : ℕ) : + HasCondDistrib (Y M) (fun ω ↦ ((history O X Y M ω, O M ω), X M ω)) (env.feedback M) + (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) := + (h.hasCondDistrib_feedback M).restrict_of_measurableSet_comap + (((h.measurable_history M).prodMk (h.measurable_obs M)).prodMk (h.measurable_action M)) + (h.measurable_feedback M) + (measurable_iff_comap_le.mp (h.measurable_history_filtrationAction M) _ + (measurableSet_comap_history_lt_stoppingTime hS M)) + +/-- On the event `{M < τ}`, if the first `M` rounds have law `μ`, the first `M + 1` rounds have +law the composition-product of `μ` with the step kernel. -/ +lemma IsAlgEnvSeq.hasLaw_history_succ_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P) + (hS : MeasurableSet S) {μ : Measure (Hist 𝓞 𝓐 𝓨 M)} + (hμ : HasLaw (history O X Y M) μ (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω})) : + HasLaw (history O X Y (M + 1)) + ((μ ⊗ₘ stepKernel alg env M).map (MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) M).symm) + (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) := + hasLaw_history_succ hμ (h.hasCondDistrib_step_restrict_lt_stoppingTime hS M) end filtration +section trajMeasure + +/-! ### The law of the stopped history + +The stopping time and the stopped history are functions of the trajectory, whose law is +determined by the algorithm and the environment (`IsAlgEnvSeq.hasLaw_trajectory`). Hence the law +of the stopped history is determined by the algorithm and the environment: it is the law +`stoppedHistMeasure alg env S` of the stopped history on the canonical space `trajMeasure`. -/ + +variable {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} + +lemma stoppingTime_eq_comp_trajectory (S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) : + stoppingTime O X Y S = stoppingTime IT.obs IT.action IT.feedback S ∘ trajectory O X Y := rfl + +lemma stoppedHist_stoppingTime_eq_comp_trajectory (S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) : + stoppedHist O X Y (stoppingTime O X Y S) = + stoppedHist IT.obs IT.action IT.feedback (stoppingTime IT.obs IT.action IT.feedback S) ∘ + trajectory O X Y := rfl + +/-- The law of the history stopped by the stopping rule `S`, for the algorithm `alg` in the +environment `env`: the law of the stopped history on the canonical space `trajMeasure alg env`. +This is the law of the stopped history for any algorithm-environment sequence +(`IsAlgEnvSeq.hasLaw_stoppedHist_stoppingTime`). -/ +noncomputable def stoppedHistMeasure (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) + (S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) : + Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) := + (trajMeasure alg env).map + (stoppedHist IT.obs IT.action IT.feedback (stoppingTime IT.obs IT.action IT.feedback S)) + +instance (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) : + IsProbabilityMeasure (stoppedHistMeasure alg env S) := by + unfold stoppedHistMeasure + infer_instance + +/-- The law of the history stopped by `S` under any algorithm-environment sequence for `alg` and +`env` is `stoppedHistMeasure alg env S`. -/ +lemma IsAlgEnvSeq.hasLaw_stoppedHist_stoppingTime {P : Measure Ω} [IsProbabilityMeasure P] + (h : IsAlgEnvSeq O X Y alg env P) (hS : MeasurableSet S) : + HasLaw (stoppedHist O X Y (stoppingTime O X Y S)) (stoppedHistMeasure alg env S) P := by + rw [stoppedHist_stoppingTime_eq_comp_trajectory] + exact ((measurable_stoppedHist IT.measurable_obs IT.measurable_action IT.measurable_feedback + (measurable_stoppingTime IT.measurable_obs IT.measurable_action IT.measurable_feedback + hS)).hasLaw_map _).comp h.hasLaw_trajectory + +end trajMeasure + end Learning From 32764dea638a2c1b4e2f64a9460a82246fd4f130 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 12 Sep 2026 08:44:01 +0200 Subject: [PATCH 4/4] use stoppedProcess --- .../SequentialLearning/IdentificationAlg.lean | 13 +- .../SequentialLearning/StoppedHistory.lean | 177 ++++++++---------- 2 files changed, 84 insertions(+), 106 deletions(-) diff --git a/LeanMachineLearning/SequentialLearning/IdentificationAlg.lean b/LeanMachineLearning/SequentialLearning/IdentificationAlg.lean index 3b9c5e5c..d12fba26 100644 --- a/LeanMachineLearning/SequentialLearning/IdentificationAlg.lean +++ b/LeanMachineLearning/SequentialLearning/IdentificationAlg.lean @@ -27,9 +27,10 @@ history at the stopping time is the output rule (`IdentAlg.IsRun`). The stopping `IdentAlg.stoppingTime A O X Y` is the stopping time `Learning.stoppingTime` of the stopping rule `A.stopSet` (the hitting time, Mathlib `hittingAfter`, of the stopping rule by the process of histories), a stopping time of the history filtration, and the history at the stopping time is -`IdentAlg.stoppedHist A O X Y` (`Learning.stoppedHist`). If the algorithm never stops, the history -at the stopping time is by convention the empty history, and the output is then drawn from the -output rule at the empty history. +`IdentAlg.stoppedHist A O X Y` (`Learning.stoppedHist`, the stopped value of the process of +histories). If the algorithm never stops, the history at the stopping time is the history of an +arbitrary, unspecified number of rounds, and the output is then drawn from the output rule at that +history. The law of the output of a run is determined by `A` and `env`: it is `A.outputMeasure env`, the law of the output on the canonical probability space of the interaction (`trajMeasure`), see @@ -104,7 +105,7 @@ noncomputable def stoppingTime : Ω → ℕ∞ := Learning.stoppingTime O X Y A. lemma stoppingTime_def : A.stoppingTime O X Y = Learning.stoppingTime O X Y A.stopSet := rfl /-- The history of the rounds played by `A`, as a history of variable length: the history stopped -at `A.stoppingTime O X Y` (the empty history if `A` never stops). -/ +at `A.stoppingTime O X Y` (the history of an arbitrary number of rounds if `A` never stops). -/ noncomputable def stoppedHist : Ω → Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n := Learning.stoppedHist O X Y (A.stoppingTime O X Y) @@ -124,8 +125,8 @@ instance (env : Environment 𝓞 𝓐 𝓨) : IsProbabilityMeasure (A.outputMeas /-- `(O, X, Y, out)` is a *run* of the identification algorithm `A` in the environment `env` on the probability space `(Ω, P)`: the observation, action and feedback processes `O`, `X`, `Y` form an algorithm-environment sequence for the sampling rule `A.alg` and `env`, and the output `out` has -conditional law `A.output` given the history at the stopping time (the empty history if `A` -never stops). -/ +conditional law `A.output` given the history at the stopping time (the history of an arbitrary +number of rounds if `A` never stops). -/ structure IsRun (env : Environment 𝓞 𝓐 𝓨) (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (out : Ω → 𝓓) (P : Measure Ω) [IsFiniteMeasure P] : Prop where /-- The actions and feedbacks are generated by the sampling rule in the environment. -/ diff --git a/LeanMachineLearning/SequentialLearning/StoppedHistory.lean b/LeanMachineLearning/SequentialLearning/StoppedHistory.lean index ff4be271..c7f6fa39 100644 --- a/LeanMachineLearning/SequentialLearning/StoppedHistory.lean +++ b/LeanMachineLearning/SequentialLearning/StoppedHistory.lean @@ -18,9 +18,10 @@ length: the interaction stops after `n` rounds if the history of these `n` round `S`. Its *stopping time* `stoppingTime O X Y S : Ω → ℕ∞` is the number of rounds played, the hitting time (Mathlib `hittingAfter`) of `S` by the process `sigmaHistory O X Y` of the histories seen as histories of variable length. For a random time `τ : Ω → ℕ∞`, `stoppedHist O X Y τ` is -the history of the first `τ` rounds, as a history of variable length: it is the stopped value -(Mathlib `stoppedValue`) of the process `sigmaHistory O X Y` at `τ`, except that when `τ = ⊤` it -is the empty history rather than an arbitrary value. +the history of the first `τ` rounds, as a history of variable length: the stopped value (Mathlib +`stoppedValue`) of the process `sigmaHistory O X Y` at `τ` (when `τ = ⊤`, this is the history of +an arbitrary, unspecified number of rounds). The history of the first `min τ M` rounds is the +stopped process (Mathlib `stoppedProcess`) `stoppedProcess (sigmaHistory O X Y) τ M`. * `stoppingTime_le_iff`, `lt_stoppingTime_iff`, `stoppingTime_eq_coe_iff`, `stoppingTime_eq_top_iff`: characterizations of the stopping time; @@ -31,8 +32,9 @@ is the empty history rather than an arbitrary value. the events `{n < stoppingTime O X Y S}` and `{stoppingTime O X Y S ≤ n}` are determined by the first `n` rounds; `IsAlgEnvSeq.isStoppingTime_stoppingTime`: `stoppingTime O X Y S` is a stopping time of the history filtration of an algorithm-environment sequence; -* `hasLaw_stoppedHist_min_add`, `hasLaw_stoppedHist_min_succ_add`: the laws of the histories - stopped at `min τ M` and `min τ (M + 1)` split according to whether `τ ≤ M`; +* `hasLaw_stoppedProcess_sigmaHistory_add`, `hasLaw_stoppedProcess_sigmaHistory_succ_add`: the + laws of the histories stopped at `min τ M` and `min τ (M + 1)` split according to whether + `τ ≤ M`; * `IsAlgEnvSeq.hasCondDistrib_step_restrict_lt_stoppingTime` (and `obs`, `action`, `feedback`): on the event `{M < τ}`, which is determined by the first `M` rounds, the round at time `M` keeps its conditional laws; `IsAlgEnvSeq.hasLaw_history_succ_restrict_lt_stoppingTime`: on this @@ -65,12 +67,12 @@ noncomputable def stoppingTime (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → (S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) : Ω → ℕ∞ := hittingAfter (sigmaHistory O X Y) S 0 -/-- The history of the first `τ ω` rounds, as a history of variable length. When `τ ω = ⊤`, this -is the empty history (Mathlib's `stoppedValue` would use an arbitrary value instead). -/ -noncomputable def stoppedHist (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (τ : Ω → ℕ∞) - (ω : Ω) : - Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n := - sigmaHistory O X Y (τ ω).toNat ω +/-- The history of the first `τ ω` rounds, as a history of variable length: the stopped value of +the process `sigmaHistory O X Y` at the random time `τ`. When `τ ω = ⊤`, this is the history of an +arbitrary, unspecified number of rounds. -/ +noncomputable def stoppedHist (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (τ : Ω → ℕ∞) : + Ω → Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n := + stoppedValue (sigmaHistory O X Y) τ variable {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} {τ : Ω → ℕ∞} {ω : Ω} {n M : ℕ} @@ -80,6 +82,9 @@ lemma sigmaHistory_apply (n : ℕ) (ω : Ω) : lemma fst_sigmaHistory (n : ℕ) (ω : Ω) : (sigmaHistory O X Y n ω).1 = n := rfl +lemma stoppedHist_def (τ : Ω → ℕ∞) : + stoppedHist O X Y τ = stoppedValue (sigmaHistory O X Y) τ := rfl + section stoppingTime lemma stoppingTime_le_iff : @@ -121,51 +126,31 @@ lemma stoppingTime_empty : stoppingTime O X Y (∅ : Set (Σ n : ℕ, Hist 𝓞 lemma stoppedHist_congr (τ τ' : Ω → ℕ∞) (h : τ ω = τ' ω) : stoppedHist O X Y τ ω = stoppedHist O X Y τ' ω := by - unfold stoppedHist - rw [h] + simp only [stoppedHist, stoppedValue, h] lemma stoppedHist_coe (M : ℕ) (ω : Ω) : - stoppedHist O X Y (fun _ ↦ (M : ℕ∞)) ω = sigmaHistory O X Y M ω := by - change sigmaHistory O X Y (M : ℕ∞).toNat ω = _ - rw [ENat.toNat_natCast] + stoppedHist O X Y (fun _ ↦ (M : ℕ∞)) ω = sigmaHistory O X Y M ω := rfl /-- The stopped history belongs to the stopping rule when the stopping time is finite. -/ lemma stoppedHist_mem_of_ne_top (h : stoppingTime O X Y S ω ≠ ⊤) : - stoppedHist O X Y (stoppingTime O X Y S) ω ∈ S := by - obtain ⟨n, hn⟩ := ENat.ne_top_iff_exists.1 h - rw [stoppedHist_congr (stoppingTime O X Y S) (fun _ ↦ (n : ℕ∞)) hn.symm, stoppedHist_coe] - exact (stoppingTime_eq_coe_iff.1 hn.symm).1 - -/-- If `τ ω ≤ M`, the history stopped at `min τ M` is the history stopped at `τ`. -/ -lemma stoppedHist_min_of_le (h : τ ω ≤ M) : - stoppedHist O X Y (fun ω ↦ min (τ ω) M) ω = stoppedHist O X Y τ ω := - stoppedHist_congr (fun ω ↦ min (τ ω) M) τ (min_eq_left h) - -/-- If `M < τ ω`, the history stopped at `min τ M` is the history of the first `M` rounds. -/ -lemma stoppedHist_min_of_lt (h : (M : ℕ∞) < τ ω) : - stoppedHist O X Y (fun ω ↦ min (τ ω) M) ω = sigmaHistory O X Y M ω := by - rw [stoppedHist_congr (fun ω ↦ min (τ ω) M) (fun _ ↦ (M : ℕ∞)) (min_eq_right h.le), - stoppedHist_coe] - -/-- If `M < τ ω`, the history stopped at `min τ (M + 1)` is the history of the first `M + 1` -rounds. -/ -lemma stoppedHist_min_succ_of_lt (h : (M : ℕ∞) < τ ω) : - stoppedHist O X Y (fun ω ↦ min (τ ω) (M + 1 : ℕ)) ω = sigmaHistory O X Y (M + 1) ω := by - rw [stoppedHist_congr (fun ω ↦ min (τ ω) (M + 1 : ℕ)) (fun _ ↦ ((M + 1 : ℕ) : ℕ∞)) - (min_eq_right ?_), stoppedHist_coe] - exact_mod_cast Order.add_one_le_of_lt h - -/-- The history stopped at `min τ M` has length at most `M`. -/ -lemma fst_stoppedHist_min_le : (stoppedHist O X Y (fun ω ↦ min (τ ω) M) ω).1 ≤ M := - ENat.toNat_le_of_le_natCast (min_le_right _ _) - -/-- The history stopped at `min τ 0` is the empty history. -/ -lemma stoppedHist_min_zero (τ : Ω → ℕ∞) : - (stoppedHist O X Y fun ω ↦ min (τ ω) ((0 : ℕ) : ℕ∞)) = fun _ ↦ ⟨0, default⟩ := by - funext ω - rw [stoppedHist_congr (fun ω ↦ min (τ ω) ((0 : ℕ) : ℕ∞)) (fun _ ↦ ((0 : ℕ) : ℕ∞)) - (min_eq_right (by simp)), stoppedHist_coe] - exact congrArg (Sigma.mk 0) (Subsingleton.elim _ _) + stoppedHist O X Y (stoppingTime O X Y S) ω ∈ S := + hittingAfter_mem_set_of_ne_top h + +/-! The history of the first `min τ M` rounds is `stoppedProcess (sigmaHistory O X Y) τ M`: it +is the history of the first `M` rounds if `M ≤ τ` (`stoppedProcess_eq_of_le`) and the history +stopped at `τ` otherwise (`stoppedProcess_eq_of_ge`). -/ + +/-- The history of the first `min τ M` rounds has length at most `M`. -/ +lemma fst_stoppedProcess_sigmaHistory_le : + (stoppedProcess (sigmaHistory O X Y) τ M ω).1 ≤ M := + (WithTop.untopA_le_iff (ne_top_of_le_ne_top (ENat.natCast_ne_top M) (min_le_left _ _))).2 + (min_le_left _ _) + +/-- The history of the first `min τ 0` rounds is the empty history. -/ +lemma stoppedProcess_sigmaHistory_zero (τ : Ω → ℕ∞) : + stoppedProcess (sigmaHistory O X Y) τ 0 = fun _ ↦ ⟨0, default⟩ := + funext fun ω ↦ (stoppedProcess_eq_of_le (zero_le : (0 : ℕ∞) ≤ τ ω)).trans + (congrArg (Sigma.mk 0) (Subsingleton.elim _ _)) end stoppingTime @@ -189,11 +174,12 @@ end natCast variable {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} -/-- The history stopped at `min τ 0` has law the Dirac mass at the empty history. -/ -lemma hasLaw_stoppedHist_min_zero (P : Measure Ω) [IsProbabilityMeasure P] (τ : Ω → ℕ∞) : - HasLaw (stoppedHist O X Y fun ω ↦ min (τ ω) ((0 : ℕ) : ℕ∞)) +/-- The history of the first `min τ 0` rounds has law the Dirac mass at the empty history. -/ +lemma hasLaw_stoppedProcess_sigmaHistory_zero (P : Measure Ω) [IsProbabilityMeasure P] + (τ : Ω → ℕ∞) : + HasLaw (stoppedProcess (sigmaHistory O X Y) τ 0) (Measure.dirac (⟨0, default⟩ : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) P := by - rw [stoppedHist_min_zero] + rw [stoppedProcess_sigmaHistory_zero] exact hasLaw_dirac_of_ae_eq (ae_eq_refl _) section measurability @@ -226,9 +212,10 @@ lemma measurable_stoppingTime (hS : MeasurableSet S) : Measurable (stoppingTime lemma measurable_stoppedHist (hτ : Measurable τ) : Measurable (stoppedHist O X Y τ) := Measurable.sigmaMk (measurable_from_top.comp hτ) (measurable_history hO hX hY) -lemma measurable_stoppedHist_min (hτ : Measurable τ) (M : ℕ) : - Measurable (stoppedHist O X Y fun ω ↦ min (τ ω) M) := - measurable_stoppedHist hO hX hY ((measurable_from_top (f := fun t : ℕ∞ ↦ min t M)).comp hτ) +lemma measurable_stoppedProcess_sigmaHistory (hτ : Measurable τ) (M : ℕ) : + Measurable (stoppedProcess (sigmaHistory O X Y) τ M) := + measurable_stoppedHist hO hX hY + ((measurable_from_top (f := fun t : ℕ∞ ↦ min (M : ℕ∞) t)).comp hτ) end measurability @@ -262,63 +249,66 @@ section law variable {P : Measure Ω} -/-- The law of the history stopped at `min τ M` splits according to whether `τ ≤ M`: on -`{τ ≤ M}` it is the law of the history stopped at `τ` (or equivalently at `min τ M`), on -`{M < τ}` it is the law of the history of the first `M` rounds. -/ -lemma hasLaw_stoppedHist_min_add (hτ : Measurable τ) {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} - {ν : Measure (Hist 𝓞 𝓐 𝓨 M)} - (hμ : HasLaw (stoppedHist O X Y fun ω ↦ min (τ ω) M) μ (P.restrict {ω | τ ω ≤ M})) +/-- The law of the history of the first `min τ M` rounds splits according to whether `τ ≤ M`: +on `{τ ≤ M}` it is the law of the history stopped at `τ` (or equivalently of the first `min τ M` +rounds), on `{M < τ}` it is the law of the history of the first `M` rounds. -/ +lemma hasLaw_stoppedProcess_sigmaHistory_add (hτ : Measurable τ) + {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} {ν : Measure (Hist 𝓞 𝓐 𝓨 M)} + (hμ : HasLaw (stoppedProcess (sigmaHistory O X Y) τ M) μ (P.restrict {ω | τ ω ≤ M})) (hν : HasLaw (history O X Y M) ν (P.restrict {ω | (M : ℕ∞) < τ ω})) : - HasLaw (stoppedHist O X Y fun ω ↦ min (τ ω) M) (μ + ν.map (Sigma.mk M)) P := by + HasLaw (stoppedProcess (sigmaHistory O X Y) τ M) (μ + ν.map (Sigma.mk M)) P := by refine hμ.add_of_restrict_compl (measurableSet_le_natCast hτ M) ?_ rw [compl_setOf_le_natCast] refine (((measurable_sigma_mk M).hasLaw_map ν).comp hν).congr ((ae_restrict_iff' (measurableSet_natCast_lt hτ M)).2 (Filter.Eventually.of_forall fun ω hω ↦ ?_)) - exact stoppedHist_min_of_lt hω + exact stoppedProcess_eq_of_le hω.le -/-- The law of the history stopped at `min τ (M + 1)` splits according to whether `τ ≤ M`: on -`{τ ≤ M}` it is the law of the history stopped at `min τ M`, on `{M < τ}` it is the law of the -history of the first `M + 1` rounds. -/ -lemma hasLaw_stoppedHist_min_succ_add (hτ : Measurable τ) +/-- The law of the history of the first `min τ (M + 1)` rounds splits according to whether +`τ ≤ M`: on `{τ ≤ M}` it is the law of the history of the first `min τ M` rounds, on `{M < τ}` it +is the law of the history of the first `M + 1` rounds. -/ +lemma hasLaw_stoppedProcess_sigmaHistory_succ_add (hτ : Measurable τ) {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} {ν : Measure (Hist 𝓞 𝓐 𝓨 (M + 1))} - (hμ : HasLaw (stoppedHist O X Y fun ω ↦ min (τ ω) M) μ (P.restrict {ω | τ ω ≤ M})) + (hμ : HasLaw (stoppedProcess (sigmaHistory O X Y) τ M) μ (P.restrict {ω | τ ω ≤ M})) (hν : HasLaw (history O X Y (M + 1)) ν (P.restrict {ω | (M : ℕ∞) < τ ω})) : - HasLaw (stoppedHist O X Y fun ω ↦ min (τ ω) (M + 1 : ℕ)) (μ + ν.map (Sigma.mk (M + 1))) P := by + HasLaw (stoppedProcess (sigmaHistory O X Y) τ (M + 1)) (μ + ν.map (Sigma.mk (M + 1))) P := by refine HasLaw.add_of_restrict_compl (measurableSet_le_natCast hτ M) ?_ ?_ · refine hμ.congr ((ae_restrict_iff' (measurableSet_le_natCast hτ M)).2 (Filter.Eventually.of_forall fun ω hω ↦ ?_)) - rw [stoppedHist_min_of_le hω, stoppedHist_min_of_le (hω.trans (by exact_mod_cast M.le_succ))] + rw [stoppedProcess_eq_of_ge hω, stoppedProcess_eq_of_ge + (hω.trans (by exact_mod_cast M.le_succ : (M : ℕ∞) ≤ ((M + 1 : ℕ) : ℕ∞)))] · rw [compl_setOf_le_natCast] refine (((measurable_sigma_mk (M + 1)).hasLaw_map ν).comp hν).congr ((ae_restrict_iff' (measurableSet_natCast_lt hτ M)).2 (Filter.Eventually.of_forall fun ω hω ↦ ?_)) - exact stoppedHist_min_succ_of_lt hω + have hω' : (M : ℕ∞) < τ ω := hω + have h_succ : ((M + 1 : ℕ) : ℕ∞) ≤ τ ω := by exact_mod_cast Order.add_one_le_of_lt hω' + exact stoppedProcess_eq_of_le h_succ -/-- The history stopped at `min τ M` has length at most `M`: its law gives measure zero to the -histories of length `> M`. -/ -lemma _root_.ProbabilityTheory.HasLaw.stoppedHist_min_apply_compl_fst_le +/-- The history of the first `min τ M` rounds has length at most `M`: its law gives measure zero +to the histories of length `> M`. -/ +lemma _root_.ProbabilityTheory.HasLaw.stoppedProcess_sigmaHistory_apply_compl_fst_le {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} - (hμ : HasLaw (stoppedHist O X Y fun ω ↦ min (τ ω) M) μ P) : + (hμ : HasLaw (stoppedProcess (sigmaHistory O X Y) τ M) μ P) : μ {h | h.1 ≤ M}ᶜ = 0 := hμ.measure_eq_zero_of_ae_notMem (measurableSet_sigma_fst_le M).compl - (ae_of_all _ fun _ h ↦ h fst_stoppedHist_min_le) + (ae_of_all _ fun _ h ↦ h fst_stoppedProcess_sigmaHistory_le) variable (hO : ∀ n, Measurable (O n)) (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n)) (hS : MeasurableSet S) include hO hX hY hS -/-- On `{τ ≤ M}`, the history stopped at `min τ M` belongs to the stopping rule: its law under -the restriction of `P` to `{τ ≤ M}` gives measure zero to `Sᶜ`. -/ -lemma _root_.ProbabilityTheory.HasLaw.stoppedHist_min_restrict_stoppingTime_le_apply_compl +/-- On `{τ ≤ M}`, the history of the first `min τ M` rounds belongs to the stopping rule: its +law under the restriction of `P` to `{τ ≤ M}` gives measure zero to `Sᶜ`. -/ +lemma _root_.ProbabilityTheory.HasLaw.stoppedProcess_sigmaHistory_stoppingTime_apply_compl {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} - (hμ : HasLaw (stoppedHist O X Y fun ω ↦ min (stoppingTime O X Y S ω) M) μ + (hμ : HasLaw (stoppedProcess (sigmaHistory O X Y) (stoppingTime O X Y S) M) μ (P.restrict {ω | stoppingTime O X Y S ω ≤ M})) : μ Sᶜ = 0 := by refine hμ.measure_eq_zero_of_ae_notMem hS.compl ((ae_restrict_iff' (measurableSet_le_natCast (measurable_stoppingTime hO hX hY hS) M)).2 (Filter.Eventually.of_forall fun ω hω h ↦ h ?_)) - rw [stoppedHist_min_of_le hω] + rw [stoppedProcess_eq_of_ge hω] exact stoppedHist_mem_of_ne_top (ne_top_of_le_ne_top (ENat.natCast_ne_top M) hω) /-- On `{M < τ}`, the history of the first `M` rounds does not belong to the stopping rule: if it @@ -414,14 +404,6 @@ of the stopped history is determined by the algorithm and the environment: it is variable {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} -lemma stoppingTime_eq_comp_trajectory (S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) : - stoppingTime O X Y S = stoppingTime IT.obs IT.action IT.feedback S ∘ trajectory O X Y := rfl - -lemma stoppedHist_stoppingTime_eq_comp_trajectory (S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) : - stoppedHist O X Y (stoppingTime O X Y S) = - stoppedHist IT.obs IT.action IT.feedback (stoppingTime IT.obs IT.action IT.feedback S) ∘ - trajectory O X Y := rfl - /-- The law of the history stopped by the stopping rule `S`, for the algorithm `alg` in the environment `env`: the law of the stopped history on the canonical space `trajMeasure alg env`. This is the law of the stopped history for any algorithm-environment sequence @@ -431,19 +413,14 @@ noncomputable def stoppedHistMeasure (alg : Algorithm 𝓞 𝓐 𝓨) (env : Env Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) := (trajMeasure alg env).map (stoppedHist IT.obs IT.action IT.feedback (stoppingTime IT.obs IT.action IT.feedback S)) - -instance (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) : - IsProbabilityMeasure (stoppedHistMeasure alg env S) := by - unfold stoppedHistMeasure - infer_instance +deriving IsProbabilityMeasure /-- The law of the history stopped by `S` under any algorithm-environment sequence for `alg` and `env` is `stoppedHistMeasure alg env S`. -/ lemma IsAlgEnvSeq.hasLaw_stoppedHist_stoppingTime {P : Measure Ω} [IsProbabilityMeasure P] (h : IsAlgEnvSeq O X Y alg env P) (hS : MeasurableSet S) : - HasLaw (stoppedHist O X Y (stoppingTime O X Y S)) (stoppedHistMeasure alg env S) P := by - rw [stoppedHist_stoppingTime_eq_comp_trajectory] - exact ((measurable_stoppedHist IT.measurable_obs IT.measurable_action IT.measurable_feedback + HasLaw (stoppedHist O X Y (stoppingTime O X Y S)) (stoppedHistMeasure alg env S) P := + ((measurable_stoppedHist IT.measurable_obs IT.measurable_action IT.measurable_feedback (measurable_stoppingTime IT.measurable_obs IT.measurable_action IT.measurable_feedback hS)).hasLaw_map _).comp h.hasLaw_trajectory