OAI/Combinatorics/ContingencyTables/Counting/CompanionRestartScheduleSemantics.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact deterministic restart budgets for the source experiment

  1. lemma OAI.ContingencyTables.CompanionRestartSchedule.configInput_data line 14
  2. lemma OAI.ContingencyTables.CompanionRestartSchedule.queryWidth_data line 21
  3. lemma OAI.ContingencyTables.CompanionRestartSchedule.proposalWidth_data line 30
  4. theorem OAI.ContingencyTables.CompanionRestartSchedule.stageWidth_data line 39
  5. theorem OAI.ContingencyTables.CompanionRestartSchedule.restartWidth_data line 53
  6. lemma OAI.ContingencyTables.CompanionRestartSchedule.initialWidths_eq line 68
  7. theorem OAI.ContingencyTables.CompanionRestartSchedule.width_data line 78

    Source documentation

    The physical width is exactly the initialized source-stage width, and depends on a history only through its length.

    theorem width_data (A : Instance (Fin m) (Fin n)) (C K H N R L : ℕ)
    (epsilon : TreeFraction.Fraction) (z : View A → ℕ)
    (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K)
…

    Mentions: OAI.ContingencyTables.RootedCatalogGrid.freeCount