From 4afb152e42446fd7d84f416777e5a6f35c075356 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 13 Jun 2026 17:27:51 +0200 Subject: [PATCH] mark two results as theorems instead of lemmas --- LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean | 2 +- LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean index b9d4c829..ae0cb0b5 100644 --- a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean +++ b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean @@ -252,7 +252,7 @@ lemma expectation_pullCount_le [Nonempty (Fin K)] · exact (measurableSet_singleton _).preimage (by fun_prop) /-- Regret bound for the ETC algorithm. -/ -lemma regret_le [Nonempty (Fin K)] +theorem regret_le [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hm : m ≠ 0) (n : ℕ) (hn : K * m ≤ n) : diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean index 231a9f86..95c19210 100644 --- a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean +++ b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean @@ -571,7 +571,7 @@ lemma expectation_pullCount_le [Nonempty (Fin K)] ring /-- Regret bound for the UCB algorithm. -/ -lemma regret_le [Nonempty (Fin K)] +theorem regret_le [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (ucbAlgorithm hK (c * σ2)) (stationaryEnv ν) P) (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 0 < c) (n : ℕ) :