Repository navigation

Adds Fenchel conjugates - #255

Open

ISIPINK wants to merge 20 commits into

LeanMachineLearning:mainfrom

ISIPINK:subgradient-fenchelconjugate

Open

Adds Fenchel conjugates#255
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
- changed from additive maps to continous linear maps
  ISIPINK
  committed
  15014af
- removed unexpanders
  ISIPINK
  committed
  3fc8c37
- changed membership to predicate for issubgradient
  ISIPINK
  committed
  723f169
- clarified uniqueness of subgradient when fderiv
  ISIPINK
  committed
  7387808
- renamed to HasSubgradientWithinAt which is more accurate
  ISIPINK
  committed
  c6edfc7
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

Commits

Commits on Sep 19, 2026

Commits on Sep 21, 2026

Commits on Sep 22, 2026

Commits on Sep 24, 2026