Repository navigation

[Draft/Roadmap] OCO regret decompositions + LEA (Hedge / Exponential Weights) regret bounds — integration plan & questions - #263

Closed

ISIPINK wants to merge 18 commits into

LeanMachineLearning:mainfrom

ISIPINK:scratch-LEA

Closed

[Draft/Roadmap] OCO regret decompositions + LEA (Hedge / Exponential Weights) regret bounds — integration plan & questions#263
ISIPINK wants to merge 18 commits into
LeanMachineLearning:mainfrom
ISIPINK:scratch-LEA

Commits on Sep 22, 2026
- added MVT for Bregman
  ISIPINK
  committed
  2b8a959
- update bregDiv_taylor to bregDiv_mvt
  ISIPINK
  committed
  780f993
- remove Analysis.Convex namespace in MVT.lean
  ISIPINK
  committed
  f687f31
Commits on Sep 23, 2026
- drafting towards LEA
  ISIPINK
  committed
  36663af
- update OMD files to use ContinuousLinearMap and HasSubgradientWithinAt
  ISIPINK
  committed
  562c1dd
- simplified strong lemma
  ISIPINK
  committed
  2a97f7b
- simplified based on strong lemma
  ISIPINK
  committed
  2cefb58
- sprinted LEA regret bound
  ISIPINK
  committed
  fa0ed92
Commits on Sep 24, 2026
- update imports and bregDiv for Analysis/Convex restructure
  ISIPINK
  committed
  7419749
- trying to figure out specilisations
  ISIPINK
  committed
  1bc1fe3
- another attempt at structuring the LEA proof
  ISIPINK
  committed
  4826ca6
Commits on Sep 25, 2026
- added wt form
  ISIPINK
  committed
  8150b83
Commits on Sep 26, 2026
- added FTRL version
  ISIPINK
  committed
  c70d35e
- compacted stability and regulariser files
  ISIPINK
  committed
  bfa01db
Commits on Sep 27, 2026
- added OGD to compare
  ISIPINK
  committed
  ac4a985
- renamed OMD to COMD2 and updated imports
  ISIPINK
  committed
  a6ad02d
- cleaned up and fixed comments
  ISIPINK
  committed
  f9a0886
Commits on Sep 28, 2026
- introduce RegretTerms for better dep tree
  ISIPINK
  committed
  57608e4