OAI/Combinatorics/ContingencyTables/Sampling/ExactCoreCost.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite-prefix cost of the actual exact sampler control graph

  1. def OAI.ContingencyTables.ExactCoreCost.retryCost line 13
  2. def OAI.ContingencyTables.ExactCoreCost.branchBudget line 16
  3. def OAI.ContingencyTables.ExactCoreCost.budget line 20
  4. theorem OAI.ContingencyTables.ExactCoreCost.prefix_correct_cost line 26

    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_cost (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) ∧
      p.cost≤budget z N := by
…

    Mentions: OAI.ContingencyTables.ExactCoreCost.budget