Adds Fenchel conjugates - #255

Open

ISIPINK wants to merge 20 commits into

LeanMachineLearning:mainfrom

ISIPINK:subgradient-fenchelconjugate

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
added fenchel conjugates
ISIPINK
committed
ff21c67
made consistent with changes to subgradient
ISIPINK
committed
85822e9
format module docstring with Main results in Calculus.lean
ISIPINK
committed
1886ef4
move FenchelConjugate to Analysis/Convex
ISIPINK
committed
8c629ef

Commits on Sep 24, 2026

sorted imports in root module
ISIPINK
committed
bc9b77e