OAI/Combinatorics/ContingencyTables/Machines/TransitionCacheRuntime.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Work bounds for cached completion multiplicities

  1. def OAI.ContingencyTables.ProfilePrograms.transitionCacheMeasure line 16

    Source documentation

    The cache is charged by the finite completion box and the requested reserved word length; no random-tape enumeration appears in this measure.

    def transitionCacheMeasure (z : TransitionCacheParameters) : ℕ :=
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.TransitionCacheParameters

  2. lemma OAI.ContingencyTables.ProfilePrograms.weight_le_cacheMeasure line 19
  3. lemma OAI.ContingencyTables.ProfilePrograms.work_completionMultiplicity line 22
  4. lemma OAI.ContingencyTables.ProfilePrograms.work_prepareTransitionCache line 50