fderiv subgradient connection, sumrule 1 fderiv - #252

Merged

RemyDegenne merged 16 commits into

LeanMachineLearning:mainfrom

ISIPINK:subgradient-deriv

Sep 22, 2026

Commits on Sep 19, 2026

defined Bregman and properties
ISIPINK
committed
e746e1e
Import Bregman in LeanMachineLearning.lean
ISIPINK
committed
1784129
Restructure Bregman module into folder with Basic.lean
ISIPINK
committed
55fa914
added subgrad def & props
ISIPINK
committed
a20977e
Restructure Subgradient module into folder with Basic.lean
ISIPINK
committed
2d7dc6a
added subgradient deriv connection
ISIPINK
committed
7b7d742
rw deriv proofs added sum rule (deriv + convex)
ISIPINK
committed
3acfb68
updated comments
ISIPINK
committed
a4b0f3e

Commits on Sep 21, 2026

Commits on Sep 22, 2026

improvements
RemyDegenne
committed
f6d0e73
move files
RemyDegenne
committed
f9400ff
Merge branch 'main' into subgradient-deriv
RemyDegenne
committed
e9cce29