Repository navigation

Example: Metropolis-Hastings and bandits - #9

Draft

RemyDegenne wants to merge 36 commits into

mainfrom

metropolisHastings

Commits on Aug 31, 2026
- extract random variables
  RemyDegenne
  committed
  da7bf52
- Update RandomDo.lean
  gaetanserre
  committed
  719d74f
- Merge branch 'main' into extractVars
  gaetanserre
  committed
  7b530f4
- Update RandomDo.lean
  gaetanserre
  committed
  c876e38
- Fix `Thompson.lean`
  gaetanserre
  committed
  b06c1ed
Commits on Sep 4, 2026
- add extend_space tactic
  RemyDegenne
  committed
  11eaad3
- mk_all
  RemyDegenne
  committed
  db6a226
- better extend_space: remove the old space
  RemyDegenne
  committed
  feff0e0
- use transfer tactic in alg_env_trace
  RemyDegenne
  committed
  969f657
- move tests to Test
  RemyDegenne
  committed
  ab21c23
- minor
  RemyDegenne
  committed
  950a0ce
- fix lint
  RemyDegenne
  committed
  ae5f52f
Commits on Sep 7, 2026
- Computable tactic
  gaetanserre
  committed
  5efde9a
- Trace
  gaetanserre
  committed
  069f744
- Add `NumLean.normal'`
  gaetanserre
  committed
  f66de1d
- Add support for `sqrt`, `log` and `expr`
  gaetanserre
  committed
  f52cc70
- Refactor
  gaetanserre
  committed
  8a7666e
Commits on Sep 8, 2026
- Better support
  gaetanserre
  committed
  c9192fd
- Binomial distribution
  gaetanserre
  committed
  c6b596f
Commits on Sep 9, 2026
- Sample examples
  gaetanserre
  committed
  dfeb187
- `mk_all`
  gaetanserre
  committed
  52eeab6
- Support for mutable expr and for loop
  gaetanserre
  committed
  cdcbf76
- Lint
  gaetanserre
  committed
  71605d2
- Test `HasGaussian`
  gaetanserre
  committed
  b8113f6
Commits on Sep 16, 2026
- improve transfer and extend_space tactics
  RemyDegenne
  committed
  dd3e68f
- improve algtrace
  RemyDegenne
  committed
  d983f5d
- Polymorphic test
  gaetanserre
  committed
  cebedb4
- Lint
  gaetanserre
  committed
  14c26e6
Commits on Sep 18, 2026
- MetropolisHastings example
  RemyDegenne
  committed
  3294a53
- Merge branch 'extractVars' into metropolisHastings
  
  RemyDegenne
  and
  claude
  committed
  ebc3634
- Update LeanMachineLearning and port to its new algorithm API
  
  RemyDegenne
  and
  claude
  committed
  dc2583f
Commits on Sep 19, 2026
- bandit examples
  RemyDegenne
  committed
  b341470
- ε-greedy bandit, with alg_env_trace
  
  RemyDegenne
  and
  claude
  committed
  389e0f7
- Fix the mk_all check: executables out of the libraries
  
  RemyDegenne
  and
  claude
  committed
  1a498ac
- Build and lint the examples in CI
  
  RemyDegenne
  and
  claude
  committed
  dcf6664
- Bandits: state regret with LML's gap, move general lemmas to ForMathlib/ForLML
  
  RemyDegenne
  and
  claude
  committed
  3909646

Commits

Commits on Aug 31, 2026

Commits on Sep 4, 2026

Commits on Sep 7, 2026

Commits on Sep 8, 2026

Commits on Sep 9, 2026

Commits on Sep 16, 2026

Commits on Sep 18, 2026

Commits on Sep 19, 2026