OAI/Combinatorics/ContingencyTables/Dense/DenseChain.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Conditional Poincaré bound for the actual dense bin chain

Both published inputs are explicit: finite-box Prékopa interpolation and finite-chain Cheeger. All margin, penalty, cut, and proposal obligations for this chain follow from the dense completion geometry.

  1. def OAI.ContingencyTables.GridBoundary.denseBinWeight line 25
  2. def OAI.ContingencyTables.GridBoundary.denseBinChain line 29
  3. def OAI.ContingencyTables.GridBoundary.denseCutConstant line 38
  4. theorem OAI.ContingencyTables.GridBoundary.corner_injective line 40
  5. theorem OAI.ContingencyTables.GridBoundary.denseBinChain_poincare line 46