Repository navigation

feat: the effective null: mixtures, convexity, solidity, setwise closure and tests - #389

Merged

lmlexplore-automation[bot] merged 5 commits into

LeanMachineLearning:mainfrom

RemyDegenne:roadmap/effective-null-worker3

Nov 14, 2026

Merged

feat: the effective null: mixtures, convexity, solidity, setwise closure and tests#389
lmlexplore-automation[bot] merged 5 commits into
LeanMachineLearning:mainfrom
RemyDegenne:roadmap/effective-null-worker3

Commits on Nov 14, 2026
- feat: the effective null: mixtures, convexity, solidity, setwise closure and tests
  
  RemyDegenne
  and
  web-flow
  committed
  b749197
- fix: address review of the effective null
  
  RemyDegenne
  and
  web-flow
  committed
  1dbe5ff
- fix: adopt the roadmap name for the test characterization of the effective null
  
  RemyDegenne
  and
  web-flow
  committed
  ce4c807
- fix: drop the finiteness hypothesis from the bounded e-variable detection lemma
  
  RemyDegenne
  and
  web-flow
  committed
  5fdb30e
- refactor: factor out the truncation of an e-variable as IsEVar.min_const
  
  RemyDegenne
  and
  web-flow
  committed
  2ff1ca4