Skip to content

Bayesian regret of Thompson sampling #61

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
RemyDegenne merged 179 commits into from
Jun 18, 2026
Merged

Bayesian regret of Thompson sampling #61

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
179 commits
Select commit Hold shift + click to select a range
eea8b66
Draft TS
paulorauber Jan 19, 2026
4f30599
Draft TS
paulorauber Jan 19, 2026
747c29f
Organize
paulorauber Jan 20, 2026
5b2b5e5
Integrate
paulorauber Jan 20, 2026
5220228
Organize TS
paulorauber Jan 20, 2026
7188eb3
Organize TS
paulorauber Jan 20, 2026
1d62922
Reorder imports
paulorauber Jan 20, 2026
904adff
Fix namespaces
paulorauber Jan 20, 2026
b5d5d12
Define posterior
paulorauber Jan 20, 2026
13a5245
Reorder arguments
paulorauber Jan 20, 2026
e1a0b27
Adopt suggestions
paulorauber Jan 21, 2026
564e904
Add documentation
paulorauber Jan 21, 2026
36ff152
Add basic properties of BayesStationaryEnv
paulorauber Jan 21, 2026
f56c8b7
Remove IT space from BayesStationaryEnv (WIP)
paulorauber Jan 23, 2026
abd75f8
Move posterior over best arm to BayesStationarEnv
paulorauber Jan 23, 2026
3a9a5b4
Organize BayesStationaryEnv
paulorauber Jan 23, 2026
5a0d994
State Bayesian regret theorem
paulorauber Jan 26, 2026
73520cd
Add extra conditions for Bayesian regret statement
paulorauber Jan 26, 2026
8f55157
Fix statement
paulorauber Jan 26, 2026
f16aeee
Merge branch 'main' into bayesian_space
paulorauber Jan 26, 2026
57033cf
Refactor
paulorauber Jan 27, 2026
d7f0594
Minor
paulorauber Jan 27, 2026
0211c1a
Finish refactor
paulorauber Jan 27, 2026
3ba0128
Minor
paulorauber Jan 27, 2026
8f0f5fe
Fix documentation
paulorauber Jan 28, 2026
56111b0
Change statement
paulorauber Feb 2, 2026
bba4396
Complete Thompson sammpling Bayesian regret bound
paulorauber Feb 10, 2026
8c11d93
Merge branch 'main' into bayesian_space
RemyDegenne Feb 10, 2026
347f2c8
fix: add import
RemyDegenne Feb 10, 2026
e614437
remove private; move lemma
RemyDegenne Feb 10, 2026
09ddc70
undo undesirable minor changes
RemyDegenne Feb 10, 2026
8c71758
minor fixes
RemyDegenne Feb 10, 2026
e15f795
lint
RemyDegenne Feb 10, 2026
b8e5a04
lint
RemyDegenne Feb 10, 2026
165024e
move uniform lemmas
RemyDegenne Feb 10, 2026
9b687fe
minor
RemyDegenne Feb 10, 2026
8f60d12
minor
RemyDegenne Feb 15, 2026
dae92ed
Merge branch 'main' into bayesian_space
RemyDegenne Feb 15, 2026
87d12e3
fix
RemyDegenne Feb 15, 2026
59f01d9
minor
RemyDegenne Feb 15, 2026
dbec0b7
Redefine IsBayesAlgEnvSeq
paulorauber Feb 18, 2026
6f0de32
Refactor HistoryDensity
paulorauber Feb 18, 2026
34a11b3
Generalize TS bound (loose)
paulorauber Feb 18, 2026
0a62626
Generalize TS Bayesian regret bound (tighter)
paulorauber Feb 18, 2026
e29b6a6
Minor
paulorauber Feb 18, 2026
fa035fe
Refactor BayesStationaryEnv (in progress)
paulorauber Feb 20, 2026
725941b
Refactor BayesStationaryEnv (in progress)
paulorauber Feb 21, 2026
ca1c1ec
Minor
paulorauber Feb 23, 2026
8f7dfa5
Swap kernel
paulorauber Feb 23, 2026
d3e9b99
Refactor BayesStationaryEnv (in progress)
paulorauber Feb 23, 2026
a3747a9
Refactor BayesStationaryEnv
paulorauber Feb 24, 2026
afc7cde
Minor
paulorauber Feb 24, 2026
f7a3e81
Minor
paulorauber Feb 24, 2026
3bf70f5
Refactor HistoryDensity (in progress)
paulorauber Feb 24, 2026
3abd375
Refactor HistoryDensity (in progress)
paulorauber Feb 25, 2026
fc462fa
Refactor HistoryDensity (in progress)
paulorauber Feb 25, 2026
f8293fd
Refactor HistoryDensity (in progress)
paulorauber Feb 25, 2026
129ed0b
Refactor HistoryDensity (in progress)
paulorauber Feb 25, 2026
4a60bf1
Refactor HistoryDensity (in progress)
paulorauber Feb 27, 2026
3d01417
Refactor HistoryDensity (in progress)
paulorauber Mar 3, 2026
8afa7c4
Minor
paulorauber Mar 3, 2026
a4e7449
Refactor HistoryDensity (in progress)
paulorauber Mar 3, 2026
37dbef2
Refactor HistoryDensity (in progress)
paulorauber Mar 4, 2026
e937043
Refactor HistoryDensity (in progress)
paulorauber Mar 4, 2026
d536774
Refactor HistoryDensity (in progress)
paulorauber Mar 4, 2026
10b4efd
Refactor AlgorithmDensity (HistoryDensity, in progress)
paulorauber Mar 5, 2026
fbbc172
Minor
paulorauber Mar 5, 2026
e51a804
Refactor AlgorithmDensity (in progress)
paulorauber Mar 6, 2026
190131c
Minor
paulorauber Mar 6, 2026
f9bd600
Remove unused code
paulorauber Mar 6, 2026
8d0d429
Revert rename
paulorauber Mar 6, 2026
cbfd74b
Refactor TS.lean (in progress)
paulorauber Mar 9, 2026
31dc860
Refactor TS.lean (in progress)
paulorauber Mar 10, 2026
cb2bd8a
Refactor TS.lean (in progress)
paulorauber Mar 11, 2026
ef8da08
Refactor TS.lean (in progress)
paulorauber Mar 13, 2026
196c9ca
Minor
paulorauber Mar 13, 2026
cd9515e
Refactor TS.lean (in progress)
paulorauber Mar 13, 2026
6a7a8e5
Minor
paulorauber Mar 13, 2026
61d7f38
Refactor TS.lean (in progress)
paulorauber Mar 17, 2026
4f36e38
Refactor TS.lean (in progress)
paulorauber Mar 17, 2026
35c01e6
Refactor TS.lean (in progress)
paulorauber Mar 17, 2026
b702a65
Refactor TS.lean (in progress)
paulorauber Mar 19, 2026
93a31d0
Refactoring SumRewards.lean (in progress)
paulorauber Mar 20, 2026
a2014e1
Refactor SumRewards.lean (in progress)
paulorauber Mar 23, 2026
319379e
Refactor SumRewards.lean (in progress)
paulorauber Mar 24, 2026
d37c489
Refactor SumRewards.lean (in progress)
paulorauber Mar 24, 2026
68ead70
Refactor SumRewards.lean (in progress)
paulorauber Mar 24, 2026
9341a1f
Refactor SumRewards.lean (in progress)
paulorauber Mar 24, 2026
c6243d5
Refactor SumRewards.lean (in progress)
paulorauber Mar 25, 2026
96008d1
Refactor SumRewards.lean (in progress)
paulorauber Mar 25, 2026
23b3ccf
Refactor SumRewards.lean (in progress)
paulorauber Mar 27, 2026
7a44518
Refactor SumRewards.lean (in progress)
paulorauber Mar 30, 2026
54e75f2
Refactor SumRewards.lean (in progress)
paulorauber Mar 30, 2026
b804a9f
Refactor SumRewards.lean (in progress)
paulorauber Mar 30, 2026
d31396b
Refactor SumRewards.lean (in progress)
paulorauber Mar 31, 2026
b872d15
Refactor SumRewards.lean
paulorauber Mar 31, 2026
7d0742f
Refactor TS.lean (in progress)
paulorauber Apr 7, 2026
382b0aa
Refactor TS.lean (in progress)
paulorauber Apr 8, 2026
f331f56
Merge remote-tracking branch 'origin/main' into bayesian_space
RemyDegenne Apr 9, 2026
8a729aa
fix
RemyDegenne Apr 9, 2026
636c66a
Refactor TS.lean (in progress)
paulorauber Apr 13, 2026
8dc181c
Refactor TS.lean (in progress)
paulorauber Apr 13, 2026
5bd9f64
Refactor TS.lean (in progress)
paulorauber Apr 14, 2026
ea80b8b
Refactor TS.lean (in progress)
paulorauber Apr 14, 2026
5ea738b
Refactor TS.lean (in progress)
paulorauber Apr 14, 2026
f2f91ad
Refactor TS.lean (in progress)
paulorauber Apr 15, 2026
498094b
Refactor TS.lean (in progress)
paulorauber Apr 16, 2026
4402052
Refactor TS.lean (in progress)
paulorauber Apr 16, 2026
0e67808
Refactor TS.lean (in progress)
paulorauber Apr 16, 2026
afc8bb5
adapt to file moves
RemyDegenne Apr 19, 2026
70b7477
Merge branch 'bayesian_space' of github.com:paulorauber/lean-bandits …
RemyDegenne Apr 19, 2026
a7e4a7b
Refactor TS.lean (in progress)
paulorauber Apr 21, 2026
2bbd57e
Refactor TS.lean
paulorauber Apr 23, 2026
e06ab09
Add Uniform
paulorauber Apr 23, 2026
5268980
Remove map_bind_condDistrib
paulorauber Apr 23, 2026
0683041
Merge branch 'main' into bayesian_space
paulorauber Apr 23, 2026
c319f37
Improve regret bound
paulorauber Apr 24, 2026
47c57de
Finish refactor (excluding Probability/ and MeasureTheory/)
paulorauber Apr 27, 2026
e3daa94
Merge branch 'main' into bayesian_space
paulorauber Apr 27, 2026
7f300db
Refactor FullSupport.lean
paulorauber May 4, 2026
263c89c
Refactor CondDistrib.lean
paulorauber May 5, 2026
91385bb
Lint
paulorauber May 5, 2026
eb2bf83
Lint
paulorauber May 5, 2026
03d1d33
Refactor HasCondDistrib.lean (in progress)
paulorauber May 7, 2026
0743219
Open defininitions from IsBayesAlgEnvSeq
paulorauber May 7, 2026
bfa8481
Move concentration inequalities out of BayesStationaryEnv
paulorauber May 7, 2026
d98e0eb
Merge branch 'main' into bayesian_space
paulorauber May 7, 2026
3b5e075
Refactor HasCondDistrib (in progress)
paulorauber May 8, 2026
a26079f
Refactor HasCondDistrib (in progress)
paulorauber May 8, 2026
f848355
Merge branch 'main' into bayesian_space
RemyDegenne May 9, 2026
30fa005
fix
RemyDegenne May 9, 2026
2575744
Merge remote-tracking branch 'origin/main' into bayesian_space
RemyDegenne May 9, 2026
1517175
fix
RemyDegenne May 9, 2026
e991c8a
Merge branch 'main' into bayesian_space
RemyDegenne May 9, 2026
71c3ba1
Refactor HasCondDistrib.lean (in progress)
paulorauber May 14, 2026
99e9336
Merge branch 'main' into bayesian_space
RemyDegenne May 15, 2026
6e42b86
Merge branch 'main' into bayesian_space
RemyDegenne May 15, 2026
3016886
Merge branch 'bayesian_space' of github.com:paulorauber/lean-bandits …
paulorauber May 15, 2026
4457e9e
Refactor HasCondDistrib.lean (in progress)
paulorauber May 15, 2026
7dbacff
Refactor HasCondDistrib.lean
paulorauber May 18, 2026
6b4b656
Refactor WithDensity.lean (in progress)
paulorauber May 18, 2026
bb4ba54
Refactor WithDensity.lean (in progress)
paulorauber May 18, 2026
a8cfc87
Refactor WithDensity.lean (in progress)
paulorauber May 19, 2026
c72c0b7
Refactor WithDensity.lean (in progress)
paulorauber May 19, 2026
7ef6621
Refactor WithDensity.lean (in progress)
paulorauber May 20, 2026
6b59c70
Refactor WithDensity.lean (in progress)
paulorauber May 20, 2026
d540261
Refactor WithDensity.lean (in progress)
paulorauber May 20, 2026
efc7914
Refactor WithDensity.lean (in progress)
paulorauber May 22, 2026
ebeb5f0
Refactor WithDensity.lean
paulorauber May 22, 2026
31d3779
Merge branch 'main' into bayesian_space
paulorauber May 22, 2026
c24b45c
Add documentation
paulorauber May 22, 2026
aa4294f
Merge branch 'main' into bayesian_space
paulorauber May 26, 2026
372ab16
Minor changes
paulorauber May 26, 2026
7ef5b11
Move trajectory
paulorauber May 26, 2026
313f878
Add AlgorithmDensityBayes.lean
paulorauber May 26, 2026
cbbb4f8
Generalize and document uniformAlgorithm
paulorauber May 26, 2026
28f7229
Fix
paulorauber May 26, 2026
9d4d784
Minor
paulorauber May 26, 2026
cedee49
Document TS
paulorauber May 29, 2026
206bc85
Document BayesStationaryEnv
paulorauber May 29, 2026
e79304d
Document AlgorithmDensityBayes
paulorauber May 29, 2026
08024c0
Merge branch 'main' into bayesian_space
paulorauber Jun 16, 2026
dac797c
Fix merge issues
paulorauber Jun 16, 2026
f011a47
Fix
paulorauber Jun 16, 2026
fe49e6b
Generalize uniformAlgorithm
paulorauber Jun 16, 2026
5af458b
Merge branch 'main' into bayesian_space
paulorauber Jun 16, 2026
b716d95
Merge branch 'main' into bayesian_space
paulorauber Jun 17, 2026
d37bbb9
Change field name
paulorauber Jun 17, 2026
76ad936
Update documentation
paulorauber Jun 17, 2026
f9aa7af
Reorder sections
paulorauber Jun 17, 2026
1ece892
Add gap properties to Regret.lean
paulorauber Jun 17, 2026
23012e0
Add BayesRegret
paulorauber Jun 17, 2026
d67251d
Documentation fix
paulorauber Jun 17, 2026
5a0b22b
Merge branch 'main' into bayesian_space
paulorauber Jun 17, 2026
773ded8
Merge branch 'main' into bayesian_space
paulorauber Jun 17, 2026
79167e3
Split definition and regret analysis
paulorauber Jun 18, 2026
8c730fe
Merge branch 'main' into bayesian_space
paulorauber Jun 18, 2026
2739c4a
Fix hist
paulorauber Jun 18, 2026
8aca9c3
Add documentation
paulorauber Jun 18, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions LeanMachineLearning.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,8 @@ public import LeanMachineLearning.ForMathlib.Probability.Kernel.KernelSub
public import LeanMachineLearning.ForMathlib.Probability.Moments.SubGaussian
public import LeanMachineLearning.ForMathlib.Probability.WithDensity
public import LeanMachineLearning.Online.Bandit.Algorithms.ETC
public import LeanMachineLearning.Online.Bandit.Algorithms.Regret.BayesRegretTS
public import LeanMachineLearning.Online.Bandit.Algorithms.TS
public import LeanMachineLearning.Online.Bandit.Algorithms.UCB
public import LeanMachineLearning.Online.Bandit.ArrayProbSpace
public import LeanMachineLearning.Online.Bandit.BayesRegret
Expand Down
Loading