Bayesian stationary environments

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

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

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 : ℕ) (ω : Ω) : ℝ :=

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 ω)

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