OAI/Combinatorics/ContingencyTables/Sampling/ExactGatePrefix.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A cheap prefix ending before rare-branch tabulation

  1. def OAI.ContingencyTables.ExactGatePrefix.output line 14
  2. def OAI.ContingencyTables.ExactGatePrefix.experiment line 19
  3. def OAI.ContingencyTables.ExactGatePrefix.budget line 22
  4. theorem OAI.ContingencyTables.ExactGatePrefix.prefix_correct_cost line 27

    Source documentation

    The rare branch is selected but its potentially large tabulation has not started at the failure endpoint of this bounded prefix.

    theorem prefix_correct_cost (z : CompletionMargins) (s : Data) :
    ∃ p,Executes program.code program.coin (output z s)
      (OnlineTree.initial program (TreeTyped.encode z) s) p ∧
      (∀ g : Option MatrixCode → ℚ,p.mean g=(experiment z).mean g) ∧ p.cost≤budget z := by
…

    Mentions: OAI.ContingencyTables.ExactGatePrefix.output, OAI.ContingencyTables.ExactGatePrefix.experiment, OAI.ContingencyTables.ExactGatePrefix.budget

  5. lemma OAI.ContingencyTables.ExactGatePrefix.failure line 98