OAI/Combinatorics/ContingencyTables/Sampling/PhysicalRepairGraph.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual small graph contains its exchanges and designated repairs

  1. def OAI.ContingencyTables.SmallGraphProfiles.repairEdges line 20
  2. def OAI.ContingencyTables.SmallGraphProfiles.fullEdges line 30
  3. def OAI.ContingencyTables.SmallGraphProfiles.fullEnergy line 34
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.physicalEnergy_le_full line 39
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.fullEnergy_nonnegative line 46
  6. theorem OAI.ContingencyTables.SmallGraphProfiles.actual_repair_energy_le line 53