Skip to content

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

lmlexplore-automation[bot] merged 3 commits into
LeanMachineLearning:mainfrom
RemyDegenne:roadmap/descent-lemma-schlisselberg2026hidden-onlinelearning

fix: credit the formal source and characterise SmoothOn on open sets

9a64c1b
Select commit
Loading
Failed to load commit list.
Sign in for the full log view