OAI/Combinatorics/ContingencyTables/Sampling/ExactIntegerPhysical.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.ExactIntegerPhysical.prefix_failure_bound line 11
2. theorem OAI.ContingencyTables.ExactIntegerPhysical.expected_time line 21

   Source documentation

   The repeating finite-state bit program has summable physical halting tail for every positive list of integer weights.

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

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