OAI/Combinatorics/ContingencyTables/Counting/CompanionInitialDraw.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Actual bounded-word initialization of the companion trace

The output is in the literal PlainIndex used by the trace chain. Its ideal rational law is exactly the source's phase-zero law; the bounded word implementation is within 2^(-h), with an explicit word length.

  1. def OAI.ContingencyTables.CompanionInitialDraw.cellEnum line 23
  2. def OAI.ContingencyTables.CompanionInitialDraw.cellCapacity line 26
  3. def OAI.ContingencyTables.CompanionInitialDraw.indexEquiv line 29
  4. def OAI.ContingencyTables.CompanionInitialDraw.idealLaw line 37
  5. theorem OAI.ContingencyTables.CompanionInitialDraw.idealLaw_mass line 41
  6. def OAI.ContingencyTables.CompanionInitialDraw.initialBits line 46
  7. def OAI.ContingencyTables.CompanionInitialDraw.draw line 48
  8. lemma OAI.ContingencyTables.CompanionInitialDraw.cellCount_bound line 53
  9. lemma OAI.ContingencyTables.CompanionInitialDraw.cellCapacity_bound line 57
  10. theorem OAI.ContingencyTables.CompanionInitialDraw.initialBits_bound line 61
  11. theorem OAI.ContingencyTables.CompanionInitialDraw.draw_error line 67
  12. def OAI.ContingencyTables.CompanionInitialDraw.precision line 83
  13. lemma OAI.ContingencyTables.CompanionInitialDraw.precision_error line 86
  14. theorem OAI.ContingencyTables.CompanionInitialDraw.initial_distance line 101

    Source documentation

    The implemented initial word is compared directly to the literal phase-zero law, so later restart estimates need no initializer oracle.

    theorem initial_distance (A : Instance I J) (h : ℕ) :
    distance (fun S => ((mapLaw (uniformLaw (α := Fin (initialBits A (precision A h)) → Bool))
…

    Mentions: OAI.ContingencyTables.CompanionInitialDraw.initialBits, OAI.ContingencyTables.CompanionInitialDraw.precision