OAI/Combinatorics/ContingencyTables/Sampling/SmallProfileFlatCode.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Flattening the two stored views for coordinate exchanges

  1. def OAI.ContingencyTables.ProfilePrograms.flattenViews line 12
  2. def OAI.ContingencyTables.ProfilePrograms.flattenViewsRealizer line 14
  3. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_flattenViews line 16
  4. def OAI.ContingencyTables.ProfilePrograms.splitViews line 18
  5. def OAI.ContingencyTables.ProfilePrograms.splitViewsRealizer line 20
  6. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_splitViews line 23
  7. lemma OAI.ContingencyTables.ProfilePrograms.split_flattenViews line 28
  8. def OAI.ContingencyTables.ProfilePrograms.codeExchange line 32
  9. def OAI.ContingencyTables.ProfilePrograms.codeExchangeRealizer line 35
  10. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_codeExchange line 40
  11. def OAI.ContingencyTables.SmallGraphProfiles.sumViewEquiv line 58
  12. def OAI.ContingencyTables.SmallGraphProfiles.flatViewEquiv line 67
  13. lemma OAI.ContingencyTables.SmallGraphProfiles.flatten_profileCode line 70
  14. theorem OAI.ContingencyTables.SmallGraphProfiles.codeExchange_eq line 86