OAI/Combinatorics/ContingencyTables/Machines/OnlineRetryRuntime.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Expected physical time of the implemented online rejection loop

  1. def OAI.ContingencyTables.OnlineRetryRuntime.machineTable line 13
  2. def OAI.ContingencyTables.OnlineRetryRuntime.initialCfg line 16
  3. def OAI.ContingencyTables.OnlineRetryRuntime.outputCfg line 19
  4. def OAI.ContingencyTables.OnlineRetryRuntime.attemptBound line 23
  5. lemma OAI.ContingencyTables.OnlineRetryRuntime.output_halted line 28
  6. theorem OAI.ContingencyTables.OnlineRetryRuntime.expected_time line 33

    Source documentation

    This statement concerns the fixed physical transition table of the online loop, not only the abstract number of rejection attempts.

    theorem expected_time (a : A) (s : TreeData.Data) (H : ℕ)
    (hH : StackCost.StackBound
      (OnlineTree.initial (OnlineIntegerRetry.program F) (TreeTyped.encode a) s).stk H)
    (hf : ∀ N,(OnlineIntegerRetry.prefixExperiment (f := f) a N).mean
…

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