OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperPreparedProposal.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Preparing the complete proposal input from binary margin lists

  1. def OAI.ContingencyTables.ProfilePrograms.squareNat line 10
  2. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_squareNat line 13
  3. def OAI.ContingencyTables.ProfilePrograms.fourthPower line 16
  4. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_fourthPower line 19
  5. def OAI.ContingencyTables.ProfilePrograms.fifthPower line 22
  6. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_fifthPower line 26
  7. def OAI.ContingencyTables.ProfilePrograms.twentiethPower line 30
  8. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_twentiethPower line 35
  9. def OAI.ContingencyTables.ProfilePrograms.marginDimension line 38
  10. def OAI.ContingencyTables.ProfilePrograms.marginDimensionRealizer line 40
  11. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_marginDimension line 48
  12. def OAI.ContingencyTables.ProfilePrograms.marginThreshold line 56
  13. def OAI.ContingencyTables.ProfilePrograms.marginThresholdRealizer line 58
  14. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_marginThreshold line 61
  15. def OAI.ContingencyTables.ProfilePrograms.marginCatalog line 64
  16. def OAI.ContingencyTables.ProfilePrograms.marginCatalogRealizer line 67
  17. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_marginCatalog line 70
  18. abbrev OAI.ContingencyTables.ProfilePrograms.RawProfileInput line 74
  19. def OAI.ContingencyTables.ProfilePrograms.prepareProfileInput line 76
  20. def OAI.ContingencyTables.ProfilePrograms.prepareProfileInputRealizer line 79
  21. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_prepareProfileInput line 83
  22. def OAI.ContingencyTables.ProfilePrograms.preparedProposal line 88
  23. def OAI.ContingencyTables.ProfilePrograms.preparedProposalRealizer line 91
  24. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_preparedProposal line 99

    Source documentation

    A single binary program computes the threshold, small-cell catalog, full neighbor list, and indexed proposal from the supplied margins.

    theorem polynomial_preparedProposal : PolynomialTime preparedProposalRealizer :=
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.preparedProposalRealizer

  25. lemma OAI.ContingencyTables.SmallGraphProfiles.marginThreshold_ofFn line 113
  26. lemma OAI.ContingencyTables.SmallGraphProfiles.prepareProfileInput_eq line 118
  27. theorem OAI.ContingencyTables.SmallGraphProfiles.preparedProposal_eq line 125