OAI/Combinatorics/ContingencyTables/Dense/DensityLayers.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A finite penalty-layer bound

The actual dense cube has bounded exponent, so a finite layer sum suffices for its normalizer. This avoids any infinite layer decomposition.

  1. def OAI.ContingencyTables.DenseWeights.layerSet line 20
  2. theorem OAI.ContingencyTables.DenseWeights.density_le_finite_layers line 23
  3. theorem OAI.ContingencyTables.DenseWeights.density_lintegral_le_layers line 55