OAI/Combinatorics/ContingencyTables/Machines/FiniteWordExecution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Executing a computed finite Boolean sampler

The program reads a fresh word on the physical online machine, preserves the input, and runs the deterministic binary sampler on that word.

  1. def OAI.ContingencyTables.FiniteWordExecution.source line 17
  2. def OAI.ContingencyTables.FiniteWordExecution.sourceRealizer line 19
  3. def OAI.ContingencyTables.FiniteWordExecution.wordMeasure line 24
  4. theorem OAI.ContingencyTables.FiniteWordExecution.work_source line 26
  5. def OAI.ContingencyTables.FiniteWordExecution.experiment line 43
  6. def OAI.ContingencyTables.FiniteWordExecution.realizer line 46
  7. theorem OAI.ContingencyTables.FiniteWordExecution.work_realizer line 56

    Source documentation

    Runtime is polynomial in the input's encoded size plus the number of fresh bits.

    theorem work_realizer {n : A → ℕ} {f : A×List Bool → B}
    {N : TreeTyped.Realizer n} {F : TreeTyped.Realizer f}
    (hN : TreeTyped.PolynomialTime N) (hF : TreeTyped.PolynomialTime F) :
    OnlineTree.WorkBound (realizer N F) (wordMeasure n) := by
…

    Mentions: OAI.ContingencyTables.FiniteWordExecution.realizer, OAI.ContingencyTables.FiniteWordExecution.wordMeasure

  8. theorem OAI.ContingencyTables.FiniteWordExecution.experiment_mean line 76