OAI/Combinatorics/ContingencyTables/Sampling/ExactCoreProgram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

One finite control graph for the ordinary and unbounded correction branches

  1. inductive OAI.ContingencyTables.ExactCoreProgram.Phase line 15
  2. instance OAI.ContingencyTables.ExactCoreProgram.(instance at line 19) line 19
  3. def OAI.ContingencyTables.ExactCoreProgram.instructions line 22
  4. def OAI.ContingencyTables.ExactCoreProgram.program line 33
  5. def OAI.ContingencyTables.ExactCoreProgram.output line 35
  6. def OAI.ContingencyTables.ExactCoreProgram.prefixExperiment line 42
  7. theorem OAI.ContingencyTables.ExactCoreProgram.prefix_correct line 47

    Source documentation

    The failed endpoint is inside the actual retry subroutine. Its successful endpoints have halted with the sampled matrix in the output register.

    theorem prefix_correct (z : CompletionMargins) (s : Data) (N : ℕ) :
    ∃ p,Executes program.code program.coin (output z s)
      (OnlineTree.initial program (TreeTyped.encode z) s) p ∧
      ∀ g : Option MatrixCode → ℚ,p.mean g=(prefixExperiment z N).mean g := by
…

    Mentions: OAI.ContingencyTables.ExactCoreProgram.output, OAI.ContingencyTables.ExactCoreProgram.program, OAI.ContingencyTables.ExactCoreProgram.prefixExperiment