Repository navigation

Issue 157 (LinUCB Matrix And Least-Squares Algebra) - #160

Open

FawadHa1der wants to merge 95 commits into

LeanMachineLearning:mainfrom

FawadHa1der:issue-157

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
- feat(LinUCB Algorithm And Process API): formalize the actual finite-action LinUCB algorithm object and its process-level API.
  FawadHa1der
  committed
  f63a9cf
- feat(LinUCB Matrix And Least-Squares Algebra): prove the linear algebra needed for ridge regression, widths, determinant ratios, and design-matrix updates.
  FawadHa1der
  committed
  c68a785
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 'main' into issue-112
  FawadHa1der
  authored
  60874d4
- Merge branch 'issue-112' into issue-157
  FawadHa1der
  committed
  b1596ee
- 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
Commits on Jul 1, 2026
- libUCB(issue-112): feedback changes to use mathlibs euclideans space
  FawadHa1der
  committed
  ac1a4ec
- Merge branch 'issue-112' into issue-157
  FawadHa1der
  committed
  98b3c32
- linUCB: implementing cascading changes because of use of Euclidian space in Dasic.lean
  FawadHa1der
  committed
  d539258
- resolve merge conflict
  FawadHa1der
  committed
  032c01a
- pulling/merging changes from main
  FawadHa1der
  committed
  c1c6ec6
- linUCB(issue-112): refactor related to removal of measurableArgmax
  FawadHa1der
  committed
  32a03c2
- Merge branch 'issue-112' into issue-157
  FawadHa1der
  committed
  39e75b4
- libUCB(issue157): linter warnings + small proof changes
  FawadHa1der
  committed
  547ddc2

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

Commits on Jul 1, 2026