OAI/Combinatorics/ContingencyTables/Sampling/PhysicalMassBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Count the small state and its large completion jointly

  1. lemma OAI.ContingencyTables.SmallGraphProfiles.hardMarginal_le_assignments line 16
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.boundedProfile_card_le line 25
  3. lemma OAI.ContingencyTables.SmallGraphProfiles.physicalAssignments_card_le line 38
  4. theorem OAI.ContingencyTables.SmallGraphProfiles.physical_total_mass_le line 52