OAI/Combinatorics/ContingencyTables/Sampling/ProfileBoxEnumeration.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Executable enumeration of the bounded two-view profile box

  1. def OAI.ContingencyTables.ProfilePrograms.profileEnumerationData line 11
  2. def OAI.ContingencyTables.ProfilePrograms.profileEnumerationDataRealizer line 14
  3. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_profileEnumerationData line 20
  4. def OAI.ContingencyTables.ProfilePrograms.profileBoxViews line 29
  5. def OAI.ContingencyTables.ProfilePrograms.profileBoxViewsRealizer line 32
  6. lemma OAI.ContingencyTables.ProfilePrograms.work_profileBoxViews line 38
  7. lemma OAI.ContingencyTables.SmallGraphProfiles.profileBoxViews_actual line 73
  8. lemma OAI.ContingencyTables.SmallGraphProfiles.profileBoxViews_decoded line 86