[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

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