OAI/Combinatorics/ContingencyTables/Sampling/SmallBalancedMarginal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Balanced marginal closure at capacities zero and one

Capacity one has two old quadratic blocks with a common mixed functional. Each fresh coordinate is isotropic. This proves closure directly on the raw integer forms, including the small cells that must be eliminated to obtain an actual tree-coordinate marginal.

  1. theorem OAI.ContingencyTables.isotropic_kernel_nonpositive line 18
  2. theorem OAI.ContingencyTables.IntegerMarginal.marginal_zero_removal_slice line 56
  3. lemma OAI.ContingencyTables.IntegerMarginal.removeOne_total line 69
  4. theorem OAI.ContingencyTables.IntegerMarginal.marginal_one_removal_slice line 81