OAI/Combinatorics/ContingencyTables/Sampling/ProfileWordProgram.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Parsing the independent words of the physical outer trial

  1. abbrev OAI.ContingencyTables.ProfilePrograms.ProfileWordSchedule line 12

    Source documentation

    The schedule contains the number of steps and the two step widths.

    abbrev ProfileWordSchedule := (ℕ×ℕ)×ℕ
  2. abbrev OAI.ContingencyTables.ProfilePrograms.ProfileWordInput line 13
  3. def OAI.ContingencyTables.ProfilePrograms.splitProfileWord line 15
  4. def OAI.ContingencyTables.ProfilePrograms.splitProfileWordRealizer line 16
  5. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_splitProfileWord line 19
  6. def OAI.ContingencyTables.ProfilePrograms.profileWordWidth line 24
  7. def OAI.ContingencyTables.ProfilePrograms.profileWordWidthRealizer line 25
  8. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_profileWordWidth line 28
  9. def OAI.ContingencyTables.ProfilePrograms.profileWalkWidth line 33
  10. def OAI.ContingencyTables.ProfilePrograms.profileWalkWidthRealizer line 34
  11. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_profileWalkWidth line 37
  12. def OAI.ContingencyTables.ProfilePrograms.profileWalkChunks line 42
  13. def OAI.ContingencyTables.ProfilePrograms.profileWalkChunksRealizer line 44
  14. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_profileWalkChunks line 48
  15. def OAI.ContingencyTables.ProfilePrograms.profileWalkWords line 53
  16. def OAI.ContingencyTables.ProfilePrograms.profileWalkWordsRealizer line 55
  17. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_profileWalkWords line 59
  18. def OAI.ContingencyTables.ProfilePrograms.profileTerminalWord line 64
  19. def OAI.ContingencyTables.ProfilePrograms.profileTerminalWordRealizer line 65
  20. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_profileTerminalWord line 68
  21. abbrev OAI.ContingencyTables.ProfilePrograms.PackedProfileTrial line 71
  22. def OAI.ContingencyTables.ProfilePrograms.profileTrialWords line 73
  23. def OAI.ContingencyTables.ProfilePrograms.profileTrialWordsRealizer line 74
  24. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_profileTrialWords line 76
  25. def OAI.ContingencyTables.ProfilePrograms.prepareProfileTrial line 79
  26. def OAI.ContingencyTables.ProfilePrograms.prepareProfileTrialRealizer line 81
  27. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_prepareProfileTrial line 86
  28. def OAI.ContingencyTables.ProfilePrograms.packedProfileTrial line 91
  29. def OAI.ContingencyTables.ProfilePrograms.packedProfileTrialRealizer line 92
  30. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_packedProfileTrial line 95
  31. lemma OAI.ContingencyTables.ProfilePrograms.splitProfileWord_ofFn line 102
  32. lemma OAI.ContingencyTables.ProfilePrograms.profileWalkWords_ofFn line 107
  33. lemma OAI.ContingencyTables.ProfilePrograms.profileTerminalWord_ofFn line 119