Repository navigation

feat: the interior of the domain of the conjugate is where tilts grow linearly - #321

Merged

lmlexplore-automation[bot] merged 3 commits into

LeanMachineLearning:mainfrom

prevostad:roadmap/conjugate-interior-coercive-worker1

Nov 13, 2026

Merged

feat: the interior of the domain of the conjugate is where tilts grow linearly#321
lmlexplore-automation[bot] merged 3 commits into
LeanMachineLearning:mainfrom
prevostad:roadmap/conjugate-interior-coercive-worker1

Commits on Nov 13, 2026
- feat: the interior of the domain of the conjugate is where tilts grow linearly
  
  prevostad
  and
  web-flow
  committed
  cbc2b73
- doc: say the conjugate is not ⊤, rather than finite, near the tilt
  
  prevostad
  and
  web-flow
  committed
  b3e312e
- doc: say the converse is proved in finite dimension, not that it needs it
  
  prevostad
  and
  web-flow
  committed
  329725d