OAI/Combinatorics/ContingencyTables/Sampling/ExactMatrixTrial.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.ExactMatrixTrial.Lookup line 14

   Source documentation

   Enumerated candidates together with a feasible fallback.

   abbrev Lookup := List (Option MatrixCode)×MatrixCode

2. abbrev OAI.ContingencyTables.ExactMatrixTrial.Input line 15
3. def OAI.ContingencyTables.ExactMatrixTrial.lookup line 17
4. def OAI.ContingencyTables.ExactMatrixTrial.lookupRealizer line 19
5. lemma OAI.ContingencyTables.ExactMatrixTrial.polynomial_lookup line 26
6. def OAI.ContingencyTables.ExactMatrixTrial.decode line 31
7. def OAI.ContingencyTables.ExactMatrixTrial.decodeRealizer line 34
8. lemma OAI.ContingencyTables.ExactMatrixTrial.polynomial_decode line 43
9. def OAI.ContingencyTables.ExactMatrixTrial.trial line 52
10. def OAI.ContingencyTables.ExactMatrixTrial.trialRealizer line 55
11. lemma OAI.ContingencyTables.ExactMatrixTrial.polynomial_trial line 63
12. lemma OAI.ContingencyTables.ExactMatrixTrial.trial_mean line 76
13. lemma OAI.ContingencyTables.ExactMatrixTrial.trial_failure line 87
14. lemma OAI.ContingencyTables.ExactMatrixTrial.prefix_mean line 95
15. lemma OAI.ContingencyTables.ExactMatrixTrial.prefix_failure line 104
16. theorem OAI.ContingencyTables.ExactMatrixTrial.expected_time line 115

    Source documentation

    Exact weighted matrix selection has a summable physical halting tail.

    theorem expected_time {K : ℕ} (candidates : Lookup) (w : Fin K → ℕ)
        (hw : 0<totalWeight w) (s : TreeData.Data) (H : ℕ)
        (hH : StackCost.StackBound
          (OnlineTree.initial (OnlineIntegerRetry.program trialRealizer)
            (TreeTyped.encode (candidates,List.ofFn w)) s).stk H) :
        Summable (PhysicalRetryTail.tail (OnlineRetryRuntime.machineTable trialRealizer)
          (OnlineRetryRuntime.initialCfg trialRealizer (candidates,List.ofFn w) s)) ∧
        (∑' t,PhysicalRetryTail.tail (OnlineRetryRuntime.machineTable trialRealizer)
          (OnlineRetryRuntime.initialCfg trialRealizer (candidates,List.ofFn w) s) t)≤
            2*(OnlineRetryRuntime.attemptBound trialRealizer (candidates,List.ofFn w) H:ℝ) :=
    …

    Mentions: OAI.ContingencyTables.ExactMatrixTrial.Lookup, OAI.ContingencyTables.OnlineIntegerRetry.program, OAI.ContingencyTables.ExactMatrixTrial.trialRealizer, OAI.ContingencyTables.PhysicalRetryTail.tail, OAI.ContingencyTables.OnlineRetryRuntime.machineTable, OAI.ContingencyTables.OnlineRetryRuntime.initialCfg, OAI.ContingencyTables.OnlineRetryRuntime.attemptBound