Repository navigation

LinUCB (Martingale And Fixed-Direction Concentration Infrastructure) - #164

Open

FawadHa1der wants to merge 97 commits into

LeanMachineLearning:mainfrom

FawadHa1der:issue-163

Commits on May 29, 2026
- feat : initial algorithm foundation for linUCB
  FawadHa1der
  committed
  fbbfe2a
- feat : initial algorithm foundation for linUCB
  FawadHa1der
  committed
  cce2458
- Merge branch 'main' into issue-112
  FawadHa1der
  committed
  86f4300
Commits on Jun 3, 2026
- feat(linUCB): proving generic one-step bound
  FawadHa1der
  committed
  7b654c3
Commits on Jun 4, 2026
- feat(linUCB): almost-sure instantaneous regret/gap bound
  FawadHa1der
  committed
  394750e
Commits on Jun 5, 2026
- feat(linUCB): all-positive-times instantaneous gap bound
  FawadHa1der
  committed
  c27ce9b
Commits on Jun 8, 2026
- feat(linUCB): cumulative regret bridge
  FawadHa1der
  committed
  9cde158
Commits on Jun 9, 2026
- sum of widths inequality using Cauchy-Schwarz from mathlib
  FawadHa1der
  committed
  af7a718
- feat(linUCB): simplify the Cauchy beta factor
  FawadHa1der
  committed
  93b64a8
Commits on Jun 10, 2026
Commits on Jun 11, 2026
- feat(linUCB): widthSqSum as quadtratic with proof
  FawadHa1der
  committed
  2eaf435
- feat(linUCB): widthSqSum as quadtratic with proof
  FawadHa1der
  committed
  32d15ef
- feat(linUCB): bridge from a quadratic-form sum bound to a widthSqSum bound
  FawadHa1der
  committed
  7bfa214
- feat(linUCB): clean up repeated term with quadraticWidthSum
  FawadHa1der
  committed
  ae83109
- feat(linUCB): lint clean up
  FawadHa1der
  committed
  5c922c7
- feat(linUCB): design matrix is just the regularization matrix
  FawadHa1der
  committed
  d2bc9e2
- feat(linUCB): proof for initial response vector
  FawadHa1der
  committed
  0b0a904
- feat(linUCB): responseVector is the LinUCB reward-feature accumulator
  FawadHa1der
  committed
  f1da71a
Commits on Jun 12, 2026
Commits on Jun 15, 2026
Commits on Jun 16, 2026
- feat(linUCB): process/history transport lemmas
  FawadHa1der
  committed
  c511de3
- feat(linUCB): compact regret theorem
  FawadHa1der
  committed
  85c4425
- feat(linUCB): direct regret theorem
  FawadHa1der
  committed
  2a7e5b1
- feat(linUCB): base case for the log-determinant elliptical-potential path
  FawadHa1der
  committed
  d568d50
- feat(linUCB): per-step potential-increment shell
  FawadHa1der
  committed
  9766e16
- feat(linUCB): one-step determinant ratio related lemmas
  FawadHa1der
  committed
  9d11254
- feat(linUCB): elliptical-potential chain related changes
  FawadHa1der
  committed
  70916c4
Commits on Jun 17, 2026
Commits on Jun 18, 2026
Commits on Jun 25, 2026
Commits on Jun 26, 2026
- feat(112): reorg the linUCB into modular files
  FawadHa1der
  committed
  c62f829
- feat(112): remove the regret file reference
  FawadHa1der
  committed
  9257d57
- Merge branch 'issue-112' into issue-157
  FawadHa1der
  committed
  2a8c5d1
- Merge branch 'issue-157' into issue-158
  FawadHa1der
  committed
  9215759
- fix merge issue
  FawadHa1der
  committed
  962cf11
- Merge branch 'main' into issue-112
  FawadHa1der
  authored
  60874d4
- Merge branch 'issue-112' into issue-157
  FawadHa1der
  committed
  b1596ee
- Merge branch 'issue-157' into issue-158
  FawadHa1der
  committed
  baa8666
- linUCB(issue-112): update the LML main import file
  FawadHa1der
  committed
  60c75ad
- linUCB(issue-112): fix author comment
  FawadHa1der
  committed
  2009014
- Merge branch 'issue-112' into issue-157
  FawadHa1der
  committed
  c05ca26
- linUCB(issue-157): update leanmachinelearning.lean imports
  FawadHa1der
  committed
  6c9a36c
- linUCB(issue-157): proof update for Matrix.mulVec_transpose
  FawadHa1der
  committed
  5fe1e27
- Merge branch 'issue-157' into issue-158
  FawadHa1der
  committed
  83757a0
- linUCB(issue-158): remove confidencenridge.lean for now
  FawadHa1der
  committed
  cb9f4c9
- linUCB(issue-158): fix linter issue
  FawadHa1der
  committed
  6e0131f
- Concentration Infrastructure proofs
  FawadHa1der
  committed
  ff055d7
- Concentration Infrastructure proofs
  FawadHa1der
  committed
  afa08d3

Commits

Commits on May 29, 2026

Commits on Jun 3, 2026

Commits on Jun 4, 2026

Commits on Jun 5, 2026

Commits on Jun 8, 2026

Commits on Jun 9, 2026

Commits on Jun 10, 2026

Commits on Jun 11, 2026

Commits on Jun 12, 2026

Commits on Jun 15, 2026

Commits on Jun 16, 2026

Commits on Jun 17, 2026

Commits on Jun 18, 2026

Commits on Jun 25, 2026

Commits on Jun 26, 2026