Skip to content

Commit 258e90f

Browse files
RemyDegenneRemyDegenne
authored
Bayesian stationary environments (#139)
2 parents cb9ba64 + 8c46327 commit 258e90f

6 files changed

Lines changed: 526 additions & 0 deletions

File tree

‎LeanMachineLearning.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,14 +21,17 @@ public import LeanMachineLearning.ForMathlib.Probability.WithDensity
2121
public import LeanMachineLearning.Online.Bandit.Algorithms.ETC
2222
public import LeanMachineLearning.Online.Bandit.Algorithms.UCB
2323
public import LeanMachineLearning.Online.Bandit.ArrayProbSpace
24+
public import LeanMachineLearning.Online.Bandit.BayesRegret
2425
public import LeanMachineLearning.Online.Bandit.Regret
2526
public import LeanMachineLearning.Online.Bandit.RewardByCountMeasure
2627
public import LeanMachineLearning.Online.Bandit.SumRewards
2728
public import LeanMachineLearning.SequentialLearning.Algorithm
2829
public import LeanMachineLearning.SequentialLearning.AlgorithmDensity
30+
public import LeanMachineLearning.SequentialLearning.AlgorithmDensityBayes
2931
public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling
3032
public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
3133
public import LeanMachineLearning.SequentialLearning.Algorithms.Uniform
34+
public import LeanMachineLearning.SequentialLearning.BayesStationaryEnv
3235
public import LeanMachineLearning.SequentialLearning.Deterministic
3336
public import LeanMachineLearning.SequentialLearning.EvaluationEnv
3437
public import LeanMachineLearning.SequentialLearning.FiniteActions

‎LeanMachineLearning/Online/Bandit/BayesRegret.lean‎

Lines changed: 148 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,148 @@
1+
/-
2+
Copyright (c) 2026 Paulo Rauber. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Paulo Rauber, Rémy Degenne
5+
-/
6+
module
7+
8+
public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax
9+
public import LeanMachineLearning.Online.Bandit.Regret
10+
11+
/-!
12+
# Bayesian regret
13+
14+
This file defines `actionMean`, `bestAction`, `gap`, and `regret` as random variables in a
15+
measurable space `Ω`. These definitions are useful when `IsBayesAlgEnvSeq Q κ alg E A Y P`.
16+
17+
Recall that `IsBayesAlgEnvSeq Q κ alg E A Y P` states that there is a measure `P : Measure Ω` such
18+
that the parameter `E : Ω → 𝓔` has law `Q` and that the sequences of actions `A : ℕ → Ω → 𝓐` and
19+
feedbacks `Y : ℕ → Ω → 𝓨` are generated by the algorithm `alg : Algorithm 𝓐 𝓨` interacting with an
20+
underlying environment that depends on `E` and `κ` (`stationaryEnv (κ.sectR (E ω))`)
21+
22+
## Main definitions
23+
24+
* `actionMean κ E a`: the mean feedback associated with action `a : 𝓐` based on the parameter `E`,
25+
which defines the underlying stationary environment together with the kernel `κ`.
26+
* `bestAction κ E`: (one of) the action(s) with the highest associated mean feedback based on `E`.
27+
* `gap κ E A n`: the difference between the highest mean feedback associated with an action and the
28+
mean feedback associated with the action at time `n` based on `E` and the sequence of actions `A`.
29+
* `regret κ E A n`: the regret at time `n` based on `E` and the sequence of actions `A`. If
30+
`IsBayesAlgEnvSeq Q κ alg E A Y P`, then `P[regret κ E A n]` is the so-called Bayesian regret of
31+
algorithm `alg` under the prior `Q`.
32+
33+
-/
34+
35+
@[expose] public section
36+
37+
open MeasureTheory ProbabilityTheory Finset
38+
39+
namespace Learning.IsBayesAlgEnvSeq
40+
41+
variable {𝓔 𝓐 𝓨 Ω : Type*}
42+
variable [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω]
43+
44+
/-- A random variable that gives the mean feedback of action `a`. -/
45+
noncomputable
46+
def actionMean (κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (a : 𝓐) (ω : Ω) : ℝ := (κ (E ω, a))[id]
47+
48+
@[fun_prop]
49+
lemma measurable_actionMean {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {a : 𝓐} (hE : Measurable E) :
50+
Measurable (actionMean κ E a) :=
51+
stronglyMeasurable_id.integral_kernel.measurable.comp (by fun_prop)
52+
53+
@[fun_prop]
54+
lemma measurable_uncurry_actionMean_comp [Countable 𝓐] [MeasurableSingletonClass 𝓐]
55+
{κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} (hE : Measurable E) {f : Ω → 𝓐} (hf : Measurable f) :
56+
Measurable (fun ω ↦ actionMean κ E (f ω) ω) := by
57+
change Measurable ((fun aω ↦ actionMean κ E aω.1 aω.2) ∘ fun ω ↦ (f ω, ω))
58+
apply Measurable.comp _ (by fun_prop)
59+
exact measurable_from_prod_countable_right (fun _ ↦ measurable_actionMean hE)
60+
61+
lemma integrable_uncurry_actionMean_comp [Countable 𝓐] [MeasurableSingletonClass 𝓐]
62+
{κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} (hE : Measurable E) {f : Ω → 𝓐} (hf : Measurable f)
63+
{P : Measure Ω} [IsFiniteMeasure P] {l u : ℝ} (hm : ∀ e a, (κ (e, a))[id] ∈ (Set.Icc l u)) :
64+
Integrable (fun ω ↦ actionMean κ E (f ω) ω) P := by
65+
refine ⟨(measurable_uncurry_actionMean_comp hE hf).aestronglyMeasurable, ?_⟩
66+
apply HasFiniteIntegral.of_bounded
67+
filter_upwards with ω using abs_le_max_abs_abs (hm (E ω) (f ω)).1 (hm (E ω) (f ω)).2
68+
69+
/-- A random variable that gives the action with the highest mean feedback. -/
70+
noncomputable
71+
def bestAction [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSingletonClass 𝓐]
72+
(κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (ω : Ω) : 𝓐 :=
73+
measurableArgmax (fun ω' a ↦ actionMean κ E a ω') ω
74+
75+
@[fun_prop]
76+
lemma measurable_bestAction [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSingletonClass 𝓐]
77+
{κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} (hE : Measurable E) : Measurable (bestAction κ E) :=
78+
measurable_measurableArgmax (by fun_prop)
79+
80+
/-- A random variable that gives the gap at time `n`. -/
81+
noncomputable
82+
def gap (κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (A : ℕ → Ω → 𝓐) (n : ℕ) (ω : Ω) : ℝ :=
83+
Bandits.gap (κ.sectR (E ω)) (A n ω)
84+
85+
omit [MeasurableSpace Ω] in
86+
/-- The gap is non-negative if the means are bounded by `u : ℝ` (even if `𝓐` is not `Finite`). -/
87+
lemma gap_nonneg_of_le {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} {ω : Ω} {u : ℝ}
88+
(h : ∀ e a, (κ (e, a))[id] ≤ u) : 0 ≤ gap κ E A n ω :=
89+
Bandits.gap_nonneg_of_le (h (E ω))
90+
91+
omit [MeasurableSpace Ω] in
92+
lemma gap_le_of_mem_Icc [Nonempty 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ}
93+
{ω : Ω} {l u : ℝ} (h : ∀ e a, (κ (e, a))[id] ∈ Set.Icc l u) : gap κ E A n ω ≤ u - l :=
94+
Bandits.gap_le_of_mem_Icc (h (E ω))
95+
96+
omit [MeasurableSpace Ω] in
97+
lemma gap_eq_sub [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSingletonClass 𝓐]
98+
{κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} {ω : Ω} :
99+
gap κ E A n ω = actionMean κ E (bestAction κ E ω) ω - actionMean κ E (A n ω) ω := by
100+
rw [gap, Bandits.gap]
101+
congr
102+
apply le_antisymm
103+
· exact ciSup_le (isMaxOn_measurableArgmax (fun ω' a ↦ actionMean κ E a ω') ω)
104+
· exact Finite.le_ciSup (fun a ↦ actionMean κ E a ω) _
105+
106+
@[fun_prop]
107+
lemma measurable_gap [Countable 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ}
108+
(hE : Measurable E) (hA : ∀ t, Measurable (A t)) : Measurable (gap κ E A n) :=
109+
(Measurable.iSup fun _ ↦ stronglyMeasurable_id.integral_kernel.measurable.comp (by fun_prop)).sub
110+
(stronglyMeasurable_id.integral_kernel.measurable.comp (by fun_prop))
111+
112+
lemma integrable_gap [Countable 𝓐] [Nonempty 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔}
113+
{A : ℕ → Ω → 𝓐} {n : ℕ} {P : Measure Ω} [IsFiniteMeasure P] (hE : Measurable E)
114+
(hA : ∀ t, Measurable (A t)) {l u : ℝ} (h : ∀ e a, (κ (e, a))[id] ∈ Set.Icc l u) :
115+
Integrable (gap κ E A n) P := by
116+
apply Integrable.of_bound (by fun_prop) (u - l)
117+
filter_upwards with ω
118+
rw [Real.norm_eq_abs, abs_of_nonneg (gap_nonneg_of_le (fun e a ↦ (h e a).2))]
119+
exact gap_le_of_mem_Icc h
120+
121+
/-- A random variable that gives the regret at time `n`. -/
122+
noncomputable
123+
def regret (κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (A : ℕ → Ω → 𝓐) (n : ℕ) (ω : Ω) : ℝ :=
124+
Bandits.regret (κ.sectR (E ω)) A n ω
125+
126+
omit [MeasurableSpace Ω] in
127+
lemma regret_eq_sum_gap {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} {ω : Ω} :
128+
regret κ E A n ω = ∑ s ∈ range n, gap κ E A s ω := by
129+
simp [regret, Bandits.regret, gap, Bandits.gap]
130+
131+
omit [MeasurableSpace Ω] in
132+
lemma regret_eq_sum_gap' {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} :
133+
regret κ E A n = fun ω ↦ ∑ s ∈ range n, gap κ E A s ω := funext fun _ ↦ regret_eq_sum_gap
134+
135+
@[fun_prop]
136+
lemma measurable_regret [Countable 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ}
137+
(hE : Measurable E) (hA : ∀ t, Measurable (A t)) : Measurable (regret κ E A n) := by
138+
rw [regret_eq_sum_gap']
139+
fun_prop
140+
141+
lemma integrable_regret [Countable 𝓐] [Nonempty 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔}
142+
{A : ℕ → Ω → 𝓐} {n : ℕ} {P : Measure Ω} [IsFiniteMeasure P] (hE : Measurable E)
143+
(hA : ∀ t, Measurable (A t)) {l u : ℝ} (h : ∀ e a, (κ (e, a))[id] ∈ Set.Icc l u) :
144+
Integrable (regret κ E A n) P := by
145+
rw [regret_eq_sum_gap']
146+
exact integrable_finsetSum _ (fun _ _ ↦ integrable_gap hE hA h)
147+
148+
end Learning.IsBayesAlgEnvSeq

‎LeanMachineLearning/Online/Bandit/Regret.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,17 @@ lemma gap_nonneg [Finite 𝓐] : 0 ≤ gap ν a := by
4242
rw [gap, sub_nonneg]
4343
exact le_ciSup (f := fun i ↦ (ν i)[id]) (by simp) a
4444

45+
omit [DecidableEq 𝓐] in
46+
/-- The gap is non-negative if the means are bounded by `u : ℝ` (even if `𝓐` is not `Finite`). -/
47+
lemma gap_nonneg_of_le {u : ℝ} (h : ∀ a, (ν a)[id] ≤ u) : 0 ≤ gap ν a := by
48+
rw [gap, sub_nonneg]
49+
exact le_ciSup ⟨u, Set.forall_mem_range.2 h⟩ a
50+
51+
omit [DecidableEq 𝓐] in
52+
lemma gap_le_of_mem_Icc [Nonempty 𝓐] {l u : ℝ} (h : ∀ a, (ν a)[id] ∈ Set.Icc l u) :
53+
gap ν a ≤ u - l := by
54+
grind [gap, ciSup_le (fun i ↦ (h i).2)]
55+
4556
/-- Regret of a sequence of pulls `k : ℕ → 𝓐` at time `t` for the reward kernel `ν ; Kernel 𝓐 ℝ`. -/
4657
noncomputable
4758
def regret (ν : Kernel 𝓐 ℝ) (A : ℕ → Ω → 𝓐) (t : ℕ) (ω : Ω) : ℝ :=

‎LeanMachineLearning/SequentialLearning/Algorithm.lean‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,15 @@ lemma IsAlgEnvSeq.measurable_step (n : ℕ) (hA : Measurable (A n))
107107
unfold IsAlgEnvSeq.step
108108
fun_prop
109109

110+
/-- A random variable that gives the sequence of action-feedback pairs. -/
111+
def trajectory (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (ω : Ω) : ℕ → 𝓐 × 𝓨 := fun n ↦ (A n ω, Y n ω)
112+
113+
@[fun_prop]
114+
lemma measurable_trajectory {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (hA : ∀ n, Measurable (A n))
115+
(hR : ∀ n, Measurable (Y n)) : Measurable (trajectory A Y) := by
116+
unfold trajectory
117+
fun_prop
118+
110119
/-- History of the algorithm-environment sequence up to time `n`. -/
111120
def IsAlgEnvSeq.hist (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) : Iic n → 𝓐 × 𝓨 :=
112121
fun i ↦ (A i ω, Y i ω)

‎LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean‎

Lines changed: 116 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
/-
2+
Copyright (c) 2026 Paulo Rauber. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Paulo Rauber
5+
-/
6+
module
7+
8+
public import LeanMachineLearning.SequentialLearning.AlgorithmDensity
9+
public import LeanMachineLearning.SequentialLearning.BayesStationaryEnv
10+
11+
/-!
12+
# Algorithm density under Bayesian stationary environments
13+
14+
This file provides results about `Algorithm.density` for the Bayesian stationary environment
15+
setting.
16+
17+
## Main results
18+
19+
Let `h : IsBayesAlgEnvSeq Q κ alg E A Y P`, `h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀`, and
20+
`hc : alg ≪ₐ alg₀`.
21+
22+
* `hasLaw_hist_withDensity h h₀ hc n`: the law of the history at time `n` under `P` is the law of
23+
the history at time `n` under `P₀` with density `alg.density alg₀ n`. Intuitively, the law of the
24+
history under `alg` can be obtained from the law of the history under `alg₀` when they are
25+
interacting with underlying stationary environments drawn from the same distribution.
26+
* `hasCondDistrib_env_hist h h₀ hc n`: the conditional distribution of `E` given the history at time
27+
`n` under `P` is almost everywhere equal to the conditional distribution of `E₀` given the history
28+
at time `n` under `P₀`. Intuitively, the posterior is independent of the algorithm used to observe
29+
the history.
30+
31+
-/
32+
33+
@[expose] public section
34+
35+
open MeasureTheory ProbabilityTheory Finset
36+
37+
namespace Learning
38+
39+
open scoped Algorithm
40+
41+
namespace IsBayesAlgEnvSeq
42+
43+
variable {𝓐 𝓨 : Type*} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
44+
variable {𝓔 : Type*} [MeasurableSpace 𝓔]
45+
variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨]
46+
variable {Q : Measure 𝓔}
47+
variable {κ : Kernel (𝓔 × 𝓐) 𝓨} [IsMarkovKernel κ]
48+
49+
variable {Ω : Type*} [MeasurableSpace Ω]
50+
variable {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
51+
variable {alg : Algorithm 𝓐 𝓨}
52+
variable {P : Measure Ω} [IsProbabilityMeasure P]
53+
54+
variable {Ω₀ : Type*} [MeasurableSpace Ω₀]
55+
variable {E₀ : Ω₀ → 𝓔} {A₀ : ℕ → Ω₀ → 𝓐} {Y₀ : ℕ → Ω₀ → 𝓨}
56+
variable {alg₀ : Algorithm 𝓐 𝓨}
57+
variable {P₀ : Measure Ω₀} [IsProbabilityMeasure P₀]
58+
59+
lemma condDistrib_hist_eq_condDistrib_hist_withDensity (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
60+
(h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) :
61+
condDistrib (IsAlgEnvSeq.hist A Y n) E P =ᵐ[Q]
62+
((condDistrib (IsAlgEnvSeq.hist A₀ Y₀ n) E₀ P₀).withDensity
63+
(fun _ ↦ alg.density alg₀ n)) := by
64+
filter_upwards [h.ae_IsAlgEnvSeq, h₀.ae_IsAlgEnvSeq, h.hasLaw_IT_hist n, h₀.hasLaw_IT_hist n]
65+
with _ hae hae₀ he he₀
66+
rw [Kernel.withDensity_apply _ (by fun_prop), ← he.map_eq, ← he₀.map_eq]
67+
exact (hae.hasLaw_hist_withDensity hae₀ hc n).map_eq
68+
69+
lemma hasLaw_hist_withDensity (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
70+
(h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) :
71+
HasLaw (IsAlgEnvSeq.hist A Y n)
72+
((P₀.map (IsAlgEnvSeq.hist A₀ Y₀ n)).withDensity (alg.density alg₀ n)) P where
73+
aemeasurable :=
74+
(IsAlgEnvSeq.measurable_hist h.measurable_action h.measurable_feedback n).aemeasurable
75+
map_eq := by
76+
have hA := h.measurable_action
77+
have hY := h.measurable_feedback
78+
have hA₀ := h₀.measurable_action
79+
have hY₀ := h₀.measurable_feedback
80+
have hE := h.measurable_param
81+
have hE₀ := h₀.measurable_param
82+
rw [← condDistrib_comp_map hE.aemeasurable (by fun_prop), h.hasLaw_env.map_eq,
83+
Measure.bind_congr_right (h.condDistrib_hist_eq_condDistrib_hist_withDensity h₀ hc n),
84+
Kernel.comp_withDensity_eq_withDensity_comp (by fun_prop),
85+
← h₀.hasLaw_env.map_eq, condDistrib_comp_map hE₀.aemeasurable (by fun_prop)]
86+
87+
variable [StandardBorelSpace 𝓔] [Nonempty 𝓔]
88+
variable [IsProbabilityMeasure Q]
89+
90+
lemma hasCondDistrib_env_hist (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
91+
(h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) :
92+
HasCondDistrib E (IsAlgEnvSeq.hist A Y n)
93+
(condDistrib E₀ (IsAlgEnvSeq.hist A₀ Y₀ n) P₀) P where
94+
aemeasurable_fst := h.measurable_param.aemeasurable
95+
aemeasurable_snd :=
96+
(IsAlgEnvSeq.measurable_hist h.measurable_action h.measurable_feedback n).aemeasurable
97+
condDistrib_eq := by
98+
have hA := h.measurable_action
99+
have hY := h.measurable_feedback
100+
have hA₀ := h₀.measurable_action
101+
have hY₀ := h₀.measurable_feedback
102+
have hE := h.measurable_param
103+
have hE₀ := h₀.measurable_param
104+
rw [condDistrib_ae_eq_iff_measure_eq_compProd _ h.measurable_param.aemeasurable,
105+
← map_swap_compProd_map_condDistrib (by fun_prop), h.hasLaw_env.map_eq,
106+
Measure.compProd_eq_compProd_withDensity_comp_snd (by fun_prop)
107+
(h.condDistrib_hist_eq_condDistrib_hist_withDensity h₀ hc n),
108+
map_swap_withDensity_comp_snd (by fun_prop),
109+
← h₀.hasLaw_env.map_eq, map_swap_compProd_map_condDistrib (by fun_prop),
110+
← compProd_map_condDistrib (by fun_prop),
111+
← Measure.compProd_withDensity_left (by fun_prop),
112+
← (hasLaw_hist_withDensity h h₀ hc n).map_eq]
113+
114+
end IsBayesAlgEnvSeq
115+
116+
end Learning

0 commit comments

Comments
 (0)