OAI/Combinatorics/ContingencyTables/Sampling/ProfileTransitionCount.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Counting the short proposal words with a shared dense cache

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

    Source documentation

    The scalar is the multiplicity of the ignored completion-bit suffix.

    abbrev TransitionCache := ResidualParameters×(ℕ×List (Option MatrixCode×ℕ))

    Mentions: OAI.ContingencyTables.ProfilePrograms.ResidualParameters

  2. abbrev OAI.ContingencyTables.ProfilePrograms.TransitionQuery line 13
  3. def OAI.ContingencyTables.ProfilePrograms.cachedWordInput line 15
  4. def OAI.ContingencyTables.ProfilePrograms.cachedWordInputRealizer line 18
  5. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_cachedWordInput line 24
  6. def OAI.ContingencyTables.ProfilePrograms.cachedWordCount line 33
  7. def OAI.ContingencyTables.ProfilePrograms.cachedWordCountRealizer line 36
  8. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_cachedWordCount line 42
  9. def OAI.ContingencyTables.ProfilePrograms.transitionCount line 49
  10. def OAI.ContingencyTables.ProfilePrograms.transitionCountRealizer line 52
  11. lemma OAI.ContingencyTables.ProfilePrograms.work_transitionCount line 61
  12. lemma OAI.ContingencyTables.ProfilePrograms.transitionCount_words line 77
  13. lemma OAI.ContingencyTables.IntegerLaw.booleanFinish_count line 88