Repository navigation

feat: smooth functions on a convex set and the descent lemma - #301

Merged

lmlexplore-automation[bot] merged 3 commits into

LeanMachineLearning:mainfrom

RemyDegenne:roadmap/descent-lemma-schlisselberg2026hidden-onlinelearning

Nov 13, 2026

Merged

feat: smooth functions on a convex set and the descent lemma#301
lmlexplore-automation[bot] merged 3 commits into
LeanMachineLearning:mainfrom
RemyDegenne:roadmap/descent-lemma-schlisselberg2026hidden-onlinelearning

Commits on Nov 12, 2026
- feat: smooth functions on a convex set and the descent lemma
  
  RemyDegenne
  and
  web-flow
  committed
  1af7cbd
Commits on Nov 13, 2026
- chore: name LMLExplore contributors in the headers of the new files
  
  RemyDegenne
  and
  claude
  committed
  97aafe3
- fix: credit the formal source and characterise SmoothOn on open sets
  
  RemyDegenne
  and
  web-flow
  committed
  9a64c1b