From edf87aee568365e462cacb9f9627b5bee2dc1caa Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Wed, 17 Jun 2026 14:30:56 +0100 Subject: [PATCH 1/3] Add files --- .../Online/Bandit/BayesRegret.lean | 148 +++++++++++ LeanMachineLearning/Online/Bandit/Regret.lean | 11 + .../AlgorithmDensityBayes.lean | 116 +++++++++ .../BayesStationaryEnv.lean | 239 ++++++++++++++++++ 4 files changed, 514 insertions(+) create mode 100644 LeanMachineLearning/Online/Bandit/BayesRegret.lean create mode 100644 LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean create mode 100644 LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean diff --git a/LeanMachineLearning/Online/Bandit/BayesRegret.lean b/LeanMachineLearning/Online/Bandit/BayesRegret.lean new file mode 100644 index 00000000..981f1c70 --- /dev/null +++ b/LeanMachineLearning/Online/Bandit/BayesRegret.lean @@ -0,0 +1,148 @@ +/- +Copyright (c) 2026 Paulo Rauber. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paulo Rauber, Rémy Degenne +-/ +module + +public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax +public import LeanMachineLearning.Online.Bandit.Regret + +/-! +# Bayesian regret + +This file defines `actionMean`, `bestAction`, `gap`, and `regret` as random variables in a +measurable space `Ω`. These definitions are useful when `IsBayesAlgEnvSeq Q κ alg E A Y P`. + +Recall that `IsBayesAlgEnvSeq Q κ alg E A Y P` states that there is a measure `P : Measure Ω` such +that the parameter `E : Ω → 𝓔` has law `Q` and that the sequences of actions `A : ℕ → Ω → 𝓐` and +feedbacks `Y : ℕ → Ω → 𝓨` are generated by the algorithm `alg : Algorithm 𝓐 𝓨` interacting with an +underlying environment that depends on `E` and `κ` (`stationaryEnv (κ.sectR (E ω))`) + +## Main definitions + +* `actionMean κ E a`: the mean feedback associated with action `a : 𝓐` based on the parameter `E`, + which defines the underlying stationary environment together with the kernel `κ`. +* `bestAction κ E`: (one of) the action(s) with the highest associated mean feedback based on `E`. +* `gap κ E A n`: the difference between the highest mean feedback associated with an action and the + mean feedback associated with the action at time `n` based on `E` and the sequence of actions `A`. +* `regret κ E A n`: the regret at time `n` based on `E` and the sequence of actions `A`. If + `IsBayesAlgEnvSeq Q κ alg E A Y P`, then `P[regret κ E A n]` is the so-called Bayesian regret of + algorithm `alg` under the prior `Q`. + +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory Finset + +namespace Learning.IsBayesAlgEnvSeq + +variable {𝓔 𝓐 𝓨 Ω : Type*} +variable [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] + +/-- A random variable that gives the mean feedback of action `a`. -/ +noncomputable +def actionMean (κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (a : 𝓐) (ω : Ω) : ℝ := (κ (E ω, a))[id] + +@[fun_prop] +lemma measurable_actionMean {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {a : 𝓐} (hE : Measurable E) : + Measurable (actionMean κ E a) := + stronglyMeasurable_id.integral_kernel.measurable.comp (by fun_prop) + +@[fun_prop] +lemma measurable_uncurry_actionMean_comp [Countable 𝓐] [MeasurableSingletonClass 𝓐] + {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} (hE : Measurable E) {f : Ω → 𝓐} (hf : Measurable f) : + Measurable (fun ω ↦ actionMean κ E (f ω) ω) := by + change Measurable ((fun aω ↦ actionMean κ E aω.1 aω.2) ∘ fun ω ↦ (f ω, ω)) + apply Measurable.comp _ (by fun_prop) + exact measurable_from_prod_countable_right (fun _ ↦ measurable_actionMean hE) + +lemma integrable_uncurry_actionMean_comp [Countable 𝓐] [MeasurableSingletonClass 𝓐] + {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} (hE : Measurable E) {f : Ω → 𝓐} (hf : Measurable f) + {P : Measure Ω} [IsFiniteMeasure P] {l u : ℝ} (hm : ∀ e a, (κ (e, a))[id] ∈ (Set.Icc l u)) : + Integrable (fun ω ↦ actionMean κ E (f ω) ω) P := by + refine ⟨(measurable_uncurry_actionMean_comp hE hf).aestronglyMeasurable, ?_⟩ + apply HasFiniteIntegral.of_bounded + filter_upwards with ω using abs_le_max_abs_abs (hm (E ω) (f ω)).1 (hm (E ω) (f ω)).2 + +/-- A random variable that gives the action with the highest mean feedback. -/ +noncomputable +def bestAction [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSingletonClass 𝓐] + (κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (ω : Ω) : 𝓐 := + measurableArgmax (fun ω' a ↦ actionMean κ E a ω') ω + +@[fun_prop] +lemma measurable_bestAction [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSingletonClass 𝓐] + {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} (hE : Measurable E) : Measurable (bestAction κ E) := + measurable_measurableArgmax (by fun_prop) + +/-- A random variable that gives the gap at time `n`. -/ +noncomputable +def gap (κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (A : ℕ → Ω → 𝓐) (n : ℕ) (ω : Ω) : ℝ := + Bandits.gap (κ.sectR (E ω)) (A n ω) + +omit [MeasurableSpace Ω] in +/-- The gap is non-negative if the means are bounded by `u : ℝ` (even if `𝓐` is not `Finite`). -/ +lemma gap_nonneg_of_le {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} {ω : Ω} {u : ℝ} + (h : ∀ e a, (κ (e, a))[id] ≤ u) : 0 ≤ gap κ E A n ω := + Bandits.gap_nonneg_of_le (h (E ω)) + +omit [MeasurableSpace Ω] in +lemma gap_le_of_mem_Icc [Nonempty 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} + {ω : Ω} {l u : ℝ} (h : ∀ e a, (κ (e, a))[id] ∈ Set.Icc l u) : gap κ E A n ω ≤ u - l := + Bandits.gap_le_of_mem_Icc (h (E ω)) + +omit [MeasurableSpace Ω] in +lemma gap_eq_sub [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSingletonClass 𝓐] + {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} {ω : Ω} : + gap κ E A n ω = actionMean κ E (bestAction κ E ω) ω - actionMean κ E (A n ω) ω := by + rw [gap, Bandits.gap] + congr + apply le_antisymm + · exact ciSup_le (isMaxOn_measurableArgmax (fun ω' a ↦ actionMean κ E a ω') ω) + · exact Finite.le_ciSup (fun a ↦ actionMean κ E a ω) _ + +@[fun_prop] +lemma measurable_gap [Countable 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} + (hE : Measurable E) (hA : ∀ t, Measurable (A t)) : Measurable (gap κ E A n) := + (Measurable.iSup fun _ ↦ stronglyMeasurable_id.integral_kernel.measurable.comp (by fun_prop)).sub + (stronglyMeasurable_id.integral_kernel.measurable.comp (by fun_prop)) + +lemma integrable_gap [Countable 𝓐] [Nonempty 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} + {A : ℕ → Ω → 𝓐} {n : ℕ} {P : Measure Ω} [IsFiniteMeasure P] (hE : Measurable E) + (hA : ∀ t, Measurable (A t)) {l u : ℝ} (h : ∀ e a, (κ (e, a))[id] ∈ Set.Icc l u) : + Integrable (gap κ E A n) P := by + apply Integrable.of_bound (by fun_prop) (u - l) + filter_upwards with ω + rw [Real.norm_eq_abs, abs_of_nonneg (gap_nonneg_of_le (fun e a ↦ (h e a).2))] + exact gap_le_of_mem_Icc h + +/-- A random variable that gives the regret at time `n`. -/ +noncomputable +def regret (κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (A : ℕ → Ω → 𝓐) (n : ℕ) (ω : Ω) : ℝ := + Bandits.regret (κ.sectR (E ω)) A n ω + +omit [MeasurableSpace Ω] in +lemma regret_eq_sum_gap {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} {ω : Ω} : + regret κ E A n ω = ∑ s ∈ range n, gap κ E A s ω := by + simp [regret, Bandits.regret, gap, Bandits.gap] + +omit [MeasurableSpace Ω] in +lemma regret_eq_sum_gap' {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} : + regret κ E A n = fun ω ↦ ∑ s ∈ range n, gap κ E A s ω := funext fun _ ↦ regret_eq_sum_gap + +@[fun_prop] +lemma measurable_regret [Countable 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} + (hE : Measurable E) (hA : ∀ t, Measurable (A t)) : Measurable (regret κ E A n) := by + rw [regret_eq_sum_gap'] + fun_prop + +lemma integrable_regret [Countable 𝓐] [Nonempty 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} + {A : ℕ → Ω → 𝓐} {n : ℕ} {P : Measure Ω} [IsFiniteMeasure P] (hE : Measurable E) + (hA : ∀ t, Measurable (A t)) {l u : ℝ} (h : ∀ e a, (κ (e, a))[id] ∈ Set.Icc l u) : + Integrable (regret κ E A n) P := by + rw [regret_eq_sum_gap'] + exact integrable_finsetSum _ (fun _ _ ↦ integrable_gap hE hA h) + +end Learning.IsBayesAlgEnvSeq diff --git a/LeanMachineLearning/Online/Bandit/Regret.lean b/LeanMachineLearning/Online/Bandit/Regret.lean index 20d68f74..c5b60e4f 100644 --- a/LeanMachineLearning/Online/Bandit/Regret.lean +++ b/LeanMachineLearning/Online/Bandit/Regret.lean @@ -42,6 +42,17 @@ lemma gap_nonneg [Finite 𝓐] : 0 ≤ gap ν a := by rw [gap, sub_nonneg] exact le_ciSup (f := fun i ↦ (ν i)[id]) (by simp) a +omit [DecidableEq 𝓐] in +/-- The gap is non-negative if the means are bounded by `u : ℝ` (even if `𝓐` is not `Finite`). -/ +lemma gap_nonneg_of_le {u : ℝ} (h : ∀ a, (ν a)[id] ≤ u) : 0 ≤ gap ν a := by + rw [gap, sub_nonneg] + exact le_ciSup ⟨u, Set.forall_mem_range.2 h⟩ a + +omit [DecidableEq 𝓐] in +lemma gap_le_of_mem_Icc [Nonempty 𝓐] {l u : ℝ} (h : ∀ a, (ν a)[id] ∈ Set.Icc l u) : + gap ν a ≤ u - l := by + grind [gap, ciSup_le (fun i ↦ (h i).2)] + /-- Regret of a sequence of pulls `k : ℕ → 𝓐` at time `t` for the reward kernel `ν ; Kernel 𝓐 ℝ`. -/ noncomputable def regret (ν : Kernel 𝓐 ℝ) (A : ℕ → Ω → 𝓐) (t : ℕ) (ω : Ω) : ℝ := diff --git a/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean b/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean new file mode 100644 index 00000000..42f381b7 --- /dev/null +++ b/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean @@ -0,0 +1,116 @@ +/- +Copyright (c) 2026 Paulo Rauber. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paulo Rauber +-/ +module + +public import LeanMachineLearning.SequentialLearning.AlgorithmDensity +public import LeanMachineLearning.SequentialLearning.BayesStationaryEnv + +/-! +# Algorithm density under Bayesian stationary environments + +This file provides results about `Algorithm.density` for the Bayesian stationary environment +setting. + +## Main results + +Let `h : IsBayesAlgEnvSeq Q κ alg E A Y P`, `h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀`, and +`hc : alg ≪ₐ alg₀`. + +* `hasLaw_hist_withDensity h h₀ hc n`: the law of the history at time `n` under `P` is the law of + the history at time `n` under `P₀` with density `alg.density alg₀ n`. Intuitively, the law of the + history under `alg` can be obtained from the law of the history under `alg₀` when they are + interacting with underlying stationary environments drawn from the same distribution. +* `hasCondDistrib_env_hist h h₀ hc n`: the conditional distribution of `E` given the history at time + `n` under `P` is almost everywhere equal to the conditional distribution of `E₀` given the history + at time `n` under `P₀`. Intuitively, the posterior is independent of the algorithm used to observe + the history. + +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory Finset + +namespace Learning + +open scoped Algorithm + +namespace IsBayesAlgEnvSeq + +variable {𝓐 𝓨 : Type*} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] +variable {𝓔 : Type*} [MeasurableSpace 𝓔] +variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] +variable {Q : Measure 𝓔} +variable {κ : Kernel (𝓔 × 𝓐) 𝓨} [IsMarkovKernel κ] + +variable {Ω : Type*} [MeasurableSpace Ω] +variable {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} +variable {alg : Algorithm 𝓐 𝓨} +variable {P : Measure Ω} [IsProbabilityMeasure P] + +variable {Ω₀ : Type*} [MeasurableSpace Ω₀] +variable {E₀ : Ω₀ → 𝓔} {A₀ : ℕ → Ω₀ → 𝓐} {Y₀ : ℕ → Ω₀ → 𝓨} +variable {alg₀ : Algorithm 𝓐 𝓨} +variable {P₀ : Measure Ω₀} [IsProbabilityMeasure P₀] + +lemma condDistrib_hist_eq_condDistrib_hist_withDensity (h : IsBayesAlgEnvSeq Q κ alg E A Y P) + (h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) : + condDistrib (IsAlgEnvSeq.hist A Y n) E P =ᵐ[Q] + ((condDistrib (IsAlgEnvSeq.hist A₀ Y₀ n) E₀ P₀).withDensity + (fun _ ↦ alg.density alg₀ n)) := by + filter_upwards [h.ae_IsAlgEnvSeq, h₀.ae_IsAlgEnvSeq, h.hasLaw_IT_hist n, h₀.hasLaw_IT_hist n] + with _ hae hae₀ he he₀ + rw [Kernel.withDensity_apply _ (by fun_prop), ← he.map_eq, ← he₀.map_eq] + exact (hae.hasLaw_hist_withDensity hae₀ hc n).map_eq + +lemma hasLaw_hist_withDensity (h : IsBayesAlgEnvSeq Q κ alg E A Y P) + (h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) : + HasLaw (IsAlgEnvSeq.hist A Y n) + ((P₀.map (IsAlgEnvSeq.hist A₀ Y₀ n)).withDensity (alg.density alg₀ n)) P where + aemeasurable := + (IsAlgEnvSeq.measurable_hist h.measurable_action h.measurable_feedback n).aemeasurable + map_eq := by + have hA := h.measurable_action + have hY := h.measurable_feedback + have hA₀ := h₀.measurable_action + have hY₀ := h₀.measurable_feedback + have hE := h.measurable_param + have hE₀ := h₀.measurable_param + rw [← condDistrib_comp_map hE.aemeasurable (by fun_prop), h.hasLaw_env.map_eq, + Measure.bind_congr_right (h.condDistrib_hist_eq_condDistrib_hist_withDensity h₀ hc n), + Kernel.comp_withDensity_eq_withDensity_comp (by fun_prop), + ← h₀.hasLaw_env.map_eq, condDistrib_comp_map hE₀.aemeasurable (by fun_prop)] + +variable [StandardBorelSpace 𝓔] [Nonempty 𝓔] +variable [IsProbabilityMeasure Q] + +lemma hasCondDistrib_env_hist (h : IsBayesAlgEnvSeq Q κ alg E A Y P) + (h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) : + HasCondDistrib E (IsAlgEnvSeq.hist A Y n) + (condDistrib E₀ (IsAlgEnvSeq.hist A₀ Y₀ n) P₀) P where + aemeasurable_fst := h.measurable_param.aemeasurable + aemeasurable_snd := + (IsAlgEnvSeq.measurable_hist h.measurable_action h.measurable_feedback n).aemeasurable + condDistrib_eq := by + have hA := h.measurable_action + have hY := h.measurable_feedback + have hA₀ := h₀.measurable_action + have hY₀ := h₀.measurable_feedback + have hE := h.measurable_param + have hE₀ := h₀.measurable_param + rw [condDistrib_ae_eq_iff_measure_eq_compProd _ h.measurable_param.aemeasurable, + ← map_swap_compProd_map_condDistrib (by fun_prop), h.hasLaw_env.map_eq, + Measure.compProd_eq_compProd_withDensity_comp_snd (by fun_prop) + (h.condDistrib_hist_eq_condDistrib_hist_withDensity h₀ hc n), + map_swap_withDensity_comp_snd (by fun_prop), + ← h₀.hasLaw_env.map_eq, map_swap_compProd_map_condDistrib (by fun_prop), + ← compProd_map_condDistrib (by fun_prop), + ← Measure.compProd_withDensity_left (by fun_prop), + ← (hasLaw_hist_withDensity h h₀ hc n).map_eq] + +end IsBayesAlgEnvSeq + +end Learning diff --git a/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean b/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean new file mode 100644 index 00000000..00fb411a --- /dev/null +++ b/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean @@ -0,0 +1,239 @@ +/- +Copyright (c) 2026 Paulo Rauber. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paulo Rauber, Rémy Degenne +-/ +module + +public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace +public import LeanMachineLearning.SequentialLearning.StationaryEnv + +/-! +# Bayesian stationary environments + +This file defines the structure `IsBayesAlgEnvSeq` and provides its basic properties. + +## Main definitions + +* `IsBayesAlgEnvSeq Q κ alg E A Y P`: states that there is a measure `P : Measure Ω` such + that the parameter `E : Ω → 𝓔` has law `Q` and that the sequences of actions `A : ℕ → Ω → 𝓐` + and feedbacks `Y : ℕ → Ω → 𝓨` are generated by the algorithm `alg : Algorithm 𝓐 𝓨` interacting + with an underlying environment that depends on `E` and `κ` (`stationaryEnv (κ.sectR (E ω))`). +* `bayesTrajMeasure Q κ alg`: for any choice of probability measure `Q : Measure 𝓔`, Markov kernel + `κ : Kernel (𝓔 × 𝓐) 𝓨`, and algorithm `alg : Algorithm 𝓐 𝓨`, provides a probability measure + `P : Measure (ℕ → 𝓐 × 𝓔 × 𝓨)` on a space that carries `E`, `A`, and `Y` such that + `IsBayesAlgEnvSeq Q κ alg E A Y P`. +* `bayesTrajMeasurePosterior Q κ alg n`: a `Kernel (Iic n → 𝓐 × 𝓨) 𝓔` that represents the posterior + over `E` given the history up to time `n` under the prior `Q` and the algorithm `alg`, assuming + that the kernel `κ` specifies how `E` gives rise to the underlying (stationary) environment. + See also `LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean`. + +## Main results + +* `ae_IsAlgEnvSeq h`: if `h : IsBayesAlgEnvSeq Q κ alg E A Y P`, for `Q`-almost every `e : 𝓔`, + `IsAlgEnvSeq A' Y' alg (stationaryEnv (κ.sectR e)) (condDistrib (trajectory A Y) E P e)` for some + sequence of actions `A' : ℕ → (ℕ → 𝓐 × 𝓨) → 𝓐` and sequence of feedbacks + `Y' : ℕ → (ℕ → 𝓐 × 𝓨) → 𝓨`. Intuitively, if the observable trajectory is generated by an + underlying parameter `e : 𝓔`, the measure that carries the `IsBayesAlgEnvSeq` structure reveals a + measure that carries an `IsAlgEnvSeq` structure under the environment `stationaryEnv (κ.sectR e)` + and the same algorithm. This allows transferring results from the `IsAlgEnvSeq` structure to the + `IsBayesAlgEnvSeq` structure. + +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory Finset +open scoped ENNReal NNReal + +namespace Learning + +variable {𝓔 𝓐 𝓨 Ω : Type*} +variable [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] + +/-- `IsBayesAlgEnvSeq Q κ alg E A Y P` states that there is a measure `P : Measure Ω` such + that the parameter `E : Ω → 𝓔` has law `Q` and that the sequences of actions `A : ℕ → Ω → 𝓐` + and feedbacks `Y : ℕ → Ω → 𝓨` are generated by the algorithm `alg : Algorithm 𝓐 𝓨` interacting + with an underlying environment that depends on `E` and `κ` (`stationaryEnv (κ.sectR (E ω))`). -/ +structure IsBayesAlgEnvSeq + [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] + (Q : Measure 𝓔) (κ : Kernel (𝓔 × 𝓐) 𝓨) (alg : Algorithm 𝓐 𝓨) + (E : Ω → 𝓔) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) + (P : Measure Ω) [IsFiniteMeasure P] : Prop where + measurable_param : Measurable E := by fun_prop + measurable_action n : Measurable (A n) := by fun_prop + measurable_feedback n : Measurable (Y n) := by fun_prop + hasLaw_env : HasLaw E Q P + hasCondDistrib_action_zero : HasCondDistrib (A 0) E (Kernel.const _ alg.p0) P + hasCondDistrib_feedback_zero : HasCondDistrib (Y 0) (fun ω ↦ (E ω, A 0 ω)) κ P + hasCondDistrib_action n : + HasCondDistrib (A (n + 1)) (fun ω ↦ (E ω, IsAlgEnvSeq.hist A Y n ω)) + ((alg.policy n).prodMkLeft _) P + hasCondDistrib_feedback n : + HasCondDistrib (Y (n + 1)) (fun ω ↦ (IsAlgEnvSeq.hist A Y n ω, E ω, A (n + 1) ω)) + (κ.prodMkLeft _) P + +namespace IsBayesAlgEnvSeq + +variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] +variable {Q : Measure 𝓔} {κ : Kernel (𝓔 × 𝓐) 𝓨} {alg : Algorithm 𝓐 𝓨} +variable {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} +variable {P : Measure Ω} [IsFiniteMeasure P] + +lemma hasLaw_action_zero [IsProbabilityMeasure P] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : + HasLaw (A 0) alg.p0 P := h.hasCondDistrib_action_zero.hasLaw_of_const + +lemma hasCondDistrib_action' (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : + HasCondDistrib (A (n + 1)) (IsAlgEnvSeq.hist A Y n) (alg.policy n) P := + (h.hasCondDistrib_action n).comp_right' (by fun_prop) + +lemma hasCondDistrib_feedback' [IsFiniteKernel κ] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : + HasCondDistrib (Y (n + 1)) (fun ω ↦ (E ω, A (n + 1) ω)) κ P := + (h.hasCondDistrib_feedback n).comp_right' (by fun_prop) + +lemma hasLaw_IT_action_zero (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : + ∀ᵐ e ∂Q, HasLaw (IT.action 0) alg.p0 (condDistrib (trajectory A Y) E P e) := by + rw [← h.hasLaw_env.map_eq] + filter_upwards [condDistrib_comp E + ((measurable_trajectory h.measurable_action h.measurable_feedback).aemeasurable) + (IT.measurable_action (𝓐 := 𝓐) (𝓨 := 𝓨) 0), + h.hasCondDistrib_action_zero.condDistrib_eq] with _ hc hcd + exact ⟨(IT.measurable_action 0).aemeasurable, by + rw [← Kernel.map_apply _ (IT.measurable_action 0), ← hc, + show IT.action 0 ∘ trajectory A Y = A 0 from rfl, hcd, Kernel.const_apply]⟩ + +lemma hasCondDistrib_IT_feedback_zero (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : + ∀ᵐ e ∂Q, HasCondDistrib (IT.feedback 0) (IT.action 0) (κ.sectR e) + (condDistrib (trajectory A Y) E P e) := by + rw [← h.hasLaw_env.map_eq] + exact h.hasCondDistrib_feedback_zero.hasCondDistrib_sectR + (IT.measurable_action 0) (IT.measurable_feedback 0) + (measurable_trajectory h.measurable_action h.measurable_feedback).aemeasurable + +lemma hasCondDistrib_IT_action (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : + ∀ᵐ e ∂Q, HasCondDistrib (IT.action (n + 1)) (IT.hist n) (alg.policy n) + (condDistrib (trajectory A Y) E P e) := by + rw [← h.hasLaw_env.map_eq] + filter_upwards [(h.hasCondDistrib_action n).hasCondDistrib_sectR + (IT.measurable_hist n) (IT.measurable_action (n + 1)) + (measurable_trajectory h.measurable_action h.measurable_feedback).aemeasurable] with _ he + rwa [Kernel.sectR_prodMkLeft] at he + +lemma hasCondDistrib_IT_feedback [IsFiniteKernel κ] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) + (n : ℕ) : + ∀ᵐ e ∂Q, HasCondDistrib (IT.feedback (n + 1)) (fun τ ↦ (IT.hist n τ, IT.action (n + 1) τ)) + ((κ.sectR e).prodMkLeft _) (condDistrib (trajectory A Y) E P e) := by + rw [← h.hasLaw_env.map_eq] + have hc : HasCondDistrib (Y (n + 1)) + (fun ω ↦ (E ω, IsAlgEnvSeq.hist A Y n ω, A (n + 1) ω)) + (κ.comap (fun (e, _, a) ↦ (e, a)) (by fun_prop)) P := + (h.hasCondDistrib_feedback n).comp_right (MeasurableEquiv.prodAssoc.symm.trans + ((MeasurableEquiv.prodCongr .prodComm (.refl _)).trans .prodAssoc)) + exact hc.hasCondDistrib_sectR ((IT.measurable_hist n).prodMk + (IT.measurable_action (n + 1))) (IT.measurable_feedback (n + 1)) + (measurable_trajectory h.measurable_action h.measurable_feedback).aemeasurable + +lemma hasLaw_IT_hist (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : + ∀ᵐ e ∂Q, HasLaw (IT.hist n) (condDistrib (IsAlgEnvSeq.hist A Y n) E P e) + (condDistrib (trajectory A Y) E P e) := by + rw [← h.hasLaw_env.map_eq, show IsAlgEnvSeq.hist A Y n = IT.hist n ∘ trajectory A Y from rfl] + filter_upwards [condDistrib_comp E + (measurable_trajectory h.measurable_action h.measurable_feedback).aemeasurable + (IT.measurable_hist n)] with _ he + exact ⟨(IT.measurable_hist n).aemeasurable, by + rw [← Kernel.map_apply _ (IT.measurable_hist n), he]⟩ + +lemma ae_IsAlgEnvSeq [IsMarkovKernel κ] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : + ∀ᵐ e ∂Q, IsAlgEnvSeq IT.action IT.feedback alg (stationaryEnv (κ.sectR e)) + (condDistrib (trajectory A Y) E P e) := by + filter_upwards [hasLaw_IT_action_zero h, hasCondDistrib_IT_feedback_zero h, + ae_all_iff.2 (hasCondDistrib_IT_action h), ae_all_iff.2 (hasCondDistrib_IT_feedback h)] + with _ ha0 hr0 hA hR + exact ⟨IT.measurable_action, IT.measurable_feedback, ha0, hr0, hA, hR⟩ + +end IsBayesAlgEnvSeq + +section IsAlgEnvSeq + +/-- An environment with observations in `𝓔 × 𝓨`. The first element `e` of an observation is +sampled from `Q` once and remains constant. The second element of an observation is sampled from +`κ (e, a)`, where `a` is the corresponding action. -/ +noncomputable +def bayesStationaryEnv (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel (𝓔 × 𝓐) 𝓨) + [IsMarkovKernel κ] : Environment 𝓐 (𝓔 × 𝓨) where + feedback n := + let g : (Iic n → 𝓐 × 𝓔 × 𝓨) × 𝓐 → 𝓔 × 𝓐 := fun (h, a) => ((h ⟨0, by simp⟩).2.1, a) + (Kernel.deterministic (Prod.fst ∘ g) (by fun_prop)) ×ₖ (κ.comap g (by fun_prop)) + ν0 := (Kernel.const _ Q) ⊗ₖ κ.swapLeft + +variable [Nonempty 𝓐] [Nonempty 𝓔] [Nonempty 𝓨] +variable [StandardBorelSpace 𝓐] [StandardBorelSpace 𝓔] [StandardBorelSpace 𝓨] +variable {Q : Measure 𝓔} [IsProbabilityMeasure Q] {κ : Kernel (𝓔 × 𝓐) 𝓨} [IsMarkovKernel κ] +variable {alg : Algorithm 𝓐 𝓨} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓔 × 𝓨} +variable {P : Measure Ω} [IsProbabilityMeasure P] + +lemma IsAlgEnvSeq.isBayesAlgEnvSeq + (h : IsAlgEnvSeq A Y (alg.prodLeft 𝓔) (bayesStationaryEnv Q κ) P) : + IsBayesAlgEnvSeq Q κ alg (fun ω ↦ (Y 0 ω).1) A (fun n ω ↦ (Y n ω).2) P where + measurable_param := (h.measurable_feedback 0).fst + measurable_action := h.measurable_action + measurable_feedback n := (h.measurable_feedback n).snd + hasLaw_env := by + apply HasCondDistrib.hasLaw_of_const + simpa [bayesStationaryEnv] using h.hasCondDistrib_feedback_zero.fst + hasCondDistrib_action_zero := by + have hc : HasCondDistrib (fun ω ↦ (Y 0 ω).1) (A 0) (Kernel.const _ Q) P := by + simpa [bayesStationaryEnv] using h.hasCondDistrib_feedback_zero.fst + simpa [h.hasLaw_action_zero.map_eq, Algorithm.prodLeft] using hc.const_map_of_const + hasCondDistrib_feedback_zero := + h.hasCondDistrib_feedback_zero.of_compProd.comp_right MeasurableEquiv.prodComm + hasCondDistrib_action n := by + let f : (Iic n → 𝓐 × 𝓔 × 𝓨) → 𝓔 × (Iic n → 𝓐 × 𝓨) := + fun h ↦ ((h ⟨0, by simp⟩).2.1, fun i ↦ ((h i).1, (h i).2.2)) + have hc : HasCondDistrib (A (n + 1)) (IsAlgEnvSeq.hist A Y n) + (((alg.policy n).comap Prod.snd (by fun_prop)).comap f (by fun_prop)) P := + h.hasCondDistrib_action n + exact hc.comp_right' (f := f) + hasCondDistrib_feedback n := by + let f : (Iic n → 𝓐 × 𝓔 × 𝓨) × 𝓐 → (Iic n → 𝓐 × 𝓨) × 𝓔 × 𝓐 := + fun p ↦ ((fun i ↦ ((p.1 i).1, (p.1 i).2.2)), (p.1 ⟨0, by simp⟩).2.1, p.2) + have hc : HasCondDistrib (fun ω ↦ (Y (n + 1) ω).2) + (fun ω ↦ (IsAlgEnvSeq.hist A Y n ω, A (n + 1) ω)) + ((Kernel.prodMkLeft ((Iic n) → 𝓐 × 𝓨) κ).comap f (by fun_prop)) P := by + simpa [bayesStationaryEnv, Kernel.prodMkLeft, ← Kernel.comap_comp_right, Function.comp_def] + using (h.hasCondDistrib_feedback n).snd + exact hc.comp_right' (by fun_prop) + +end IsAlgEnvSeq + +namespace IT + +/-- A measure `P` on a measurable space that carries random variables `E`, `A`, and `Y` such that +`IsBayesAlgEnvSeq Q κ alg E A Y P`. -/ +noncomputable +def bayesTrajMeasure (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel (𝓔 × 𝓐) 𝓨) + [IsMarkovKernel κ] (alg : Algorithm 𝓐 𝓨) : Measure (ℕ → 𝓐 × 𝓔 × 𝓨) := + trajMeasure (alg.prodLeft 𝓔) (bayesStationaryEnv Q κ) +deriving IsProbabilityMeasure + +lemma isBayesAlgEnvSeq_bayesTrajMeasure + [StandardBorelSpace 𝓐] [Nonempty 𝓐] + [StandardBorelSpace 𝓔] [Nonempty 𝓔] + [StandardBorelSpace 𝓨] [Nonempty 𝓨] + (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel (𝓔 × 𝓐) 𝓨) [IsMarkovKernel κ] + (alg : Algorithm 𝓐 𝓨) : + IsBayesAlgEnvSeq Q κ alg (fun ω ↦ (ω 0).2.1) action (fun n ω ↦ (ω n).2.2) + (bayesTrajMeasure Q κ alg) := (isAlgEnvSeq_trajMeasure _ _).isBayesAlgEnvSeq + +/-- A kernel that represents the posterior over `E` given the history up to time `n`. -/ +noncomputable +def bayesTrajMeasurePosterior [StandardBorelSpace 𝓔] [Nonempty 𝓔] + (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel (𝓔 × 𝓐) 𝓨) [IsMarkovKernel κ] + (alg : Algorithm 𝓐 𝓨) (n : ℕ) : Kernel (Iic n → 𝓐 × 𝓨) 𝓔 := + condDistrib (fun ω ↦ (ω 0).2.1) (IsAlgEnvSeq.hist action (fun n ω ↦ (ω n).2.2) n) + (bayesTrajMeasure Q κ alg) +deriving IsMarkovKernel + +end IT + +end Learning From 4fe36ac89289d541bd4ff03b14c6f172dd1ad783 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Wed, 17 Jun 2026 14:39:28 +0100 Subject: [PATCH 2/3] Update LeanMachineLearning.lean --- LeanMachineLearning.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 9f0ad402..9f11b08c 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -21,14 +21,17 @@ public import LeanMachineLearning.ForMathlib.Probability.WithDensity public import LeanMachineLearning.Online.Bandit.Algorithms.ETC public import LeanMachineLearning.Online.Bandit.Algorithms.UCB public import LeanMachineLearning.Online.Bandit.ArrayProbSpace +public import LeanMachineLearning.Online.Bandit.BayesRegret public import LeanMachineLearning.Online.Bandit.Regret public import LeanMachineLearning.Online.Bandit.RewardByCountMeasure public import LeanMachineLearning.Online.Bandit.SumRewards public import LeanMachineLearning.SequentialLearning.Algorithm public import LeanMachineLearning.SequentialLearning.AlgorithmDensity +public import LeanMachineLearning.SequentialLearning.AlgorithmDensityBayes public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin public import LeanMachineLearning.SequentialLearning.Algorithms.Uniform +public import LeanMachineLearning.SequentialLearning.BayesStationaryEnv public import LeanMachineLearning.SequentialLearning.Deterministic public import LeanMachineLearning.SequentialLearning.EvaluationEnv public import LeanMachineLearning.SequentialLearning.FiniteActions From 8c463273cd5410338dfea4115ef8acb4719cc7c2 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Wed, 17 Jun 2026 14:49:18 +0100 Subject: [PATCH 3/3] Add Algorithm.lean --- LeanMachineLearning/SequentialLearning/Algorithm.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean index 65095fce..4a47a8d6 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithm.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean @@ -107,6 +107,15 @@ lemma IsAlgEnvSeq.measurable_step (n : ℕ) (hA : Measurable (A n)) unfold IsAlgEnvSeq.step fun_prop +/-- A random variable that gives the sequence of action-feedback pairs. -/ +def trajectory (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (ω : Ω) : ℕ → 𝓐 × 𝓨 := fun n ↦ (A n ω, Y n ω) + +@[fun_prop] +lemma measurable_trajectory {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (hA : ∀ n, Measurable (A n)) + (hR : ∀ n, Measurable (Y n)) : Measurable (trajectory A Y) := by + unfold trajectory + fun_prop + /-- History of the algorithm-environment sequence up to time `n`. -/ def IsAlgEnvSeq.hist (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) : Iic n → 𝓐 × 𝓨 := fun i ↦ (A i ω, Y i ω)