OAI/Combinatorics/ContingencyTables/Machines/OnlineIntegerRetry.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.ContingencyTables.OnlineIntegerRetry.Label line 15
2. instance OAI.ContingencyTables.OnlineIntegerRetry.(instance at line 19) line 19
3. def OAI.ContingencyTables.OnlineIntegerRetry.prepareProc line 22
4. def OAI.ContingencyTables.OnlineIntegerRetry.retryProc line 24
5. def OAI.ContingencyTables.OnlineIntegerRetry.finishProc line 27
6. lemma OAI.ContingencyTables.OnlineIntegerRetry.prepare_exec line 31
7. lemma OAI.ContingencyTables.OnlineIntegerRetry.retry_exec line 36
8. lemma OAI.ContingencyTables.OnlineIntegerRetry.finish_exec line 42
9. def OAI.ContingencyTables.OnlineIntegerRetry.instructions line 53
10. def OAI.ContingencyTables.OnlineIntegerRetry.program line 63

    Source documentation

    A single finite control graph, independent of the number of retries.

    def program : OnlineProc.Proc (K Reg) := OnlineControl.compile (instructions F)

    Mentions: OAI.ContingencyTables.OnlineIntegerRetry.instructions

11. def OAI.ContingencyTables.OnlineIntegerRetry.output line 65
12. def OAI.ContingencyTables.OnlineIntegerRetry.prefixExperiment line 69
13. def OAI.ContingencyTables.OnlineIntegerRetry.stepCost line 73
14. lemma OAI.ContingencyTables.OnlineIntegerRetry.prefix_step line 75
15. theorem OAI.ContingencyTables.OnlineIntegerRetry.prefix_correct line 142

    Source documentation

    All finite prefix laws belong to the same fixed looping program. Failure leaves the original input at the live retry entry.

    theorem prefix_correct (a : A) (s : Data) (N : ℕ) :
        ∃ q,OnlineRetryPrefix.At (instructions F) (output a s)
          (some .prepare) (env (TreeTyped.encode a) .nil s) q ∧
          (∀ g : Option B → ℚ,q.mean g=(prefixExperiment (f := f) a N).mean g) ∧
    …

    Mentions: OAI.ContingencyTables.OnlineRetryPrefix.At, OAI.ContingencyTables.OnlineIntegerRetry.instructions, OAI.ContingencyTables.OnlineIntegerRetry.output, OAI.ContingencyTables.OnlineIntegerRetry.prefixExperiment

16. theorem OAI.ContingencyTables.OnlineIntegerRetry.physical_prefix line 163

    Source documentation

    The finite prefixes also execute on the actual compiled tape machine. The failed endpoint still has a live control state.

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

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