OAI/Combinatorics/ContingencyTables/Dense/GridPartition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Partition of cube mass by the finite bins

The union misses only grid hyperplanes. Thus a predicate and its complement have continuous masses summing to the cube mass, which lets the conductance argument select the smaller continuous side.

  1. theorem OAI.ContingencyTables.GridBoundary.cube_ae_all_bins line 20
  2. theorem OAI.ContingencyTables.GridBoundary.cube_integral_bins line 36
  3. theorem OAI.ContingencyTables.GridBoundary.selected_complement_integral line 45
  4. theorem OAI.ContingencyTables.GridBoundary.selected_mass_positive line 67