OAI/Combinatorics/ContingencyTables/Sampling/PhysicalRetryIteration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.PhysicalRetryIteration.repeatTrial line 10
2. theorem OAI.ContingencyTables.PhysicalRetryIteration.repeat_cost line 14
3. theorem OAI.ContingencyTables.PhysicalRetryIteration.repeat_implements line 25
4. lemma OAI.ContingencyTables.PhysicalRetryIteration.repeat_mean line 38
5. theorem OAI.ContingencyTables.PhysicalRetryIteration.linear_physical_prefix line 56

   Source documentation

   Compiling one attempt and composing its execution proof avoids any growth of the compiler overhead with the number of preceding attempts.

   theorem linear_physical_prefix (a : A) (s : TreeData.Data) (H : ℕ)
       (hH : StackCost.StackBound
         (OnlineTree.initial (OnlineIntegerRetry.program F) (TreeTyped.encode a) s).stk H)
       (N : ℕ) :
       ∃ q,PhysicalPost.Implements
         (OnlineStack.table (OnlineIntegerRetry.program F).code (OnlineIntegerRetry.program F).coin)
         (fun b => OnlineStack.cfg (OnlineControl.cfg (OnlineIntegerRetry.instructions F)
           (OnlineIntegerRetry.output a s b).1 (OnlineIntegerRetry.output a s b).2))
         (OnlineStack.cfg (OnlineTree.initial (OnlineIntegerRetry.program F) (TreeTyped.encode a) s)) q ∧
         (∀ g : Option B → ℚ,q.mean g=
           (OnlineIntegerRetry.prefixExperiment (f := f) a N).mean g) ∧
   …

   Mentions: OAI.ContingencyTables.OnlineIntegerRetry.program, OAI.ContingencyTables.OnlineIntegerRetry.instructions, OAI.ContingencyTables.OnlineIntegerRetry.output, OAI.ContingencyTables.OnlineIntegerRetry.prefixExperiment