OAI/Combinatorics/ContingencyTables/Rooted/RootedRestartPrefix.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Restart accuracy from only the learned multiplier prefix

The horizon controls the fixed mixing schedule. Goodness is required only at the parameters which the actual restart has visited.

  1. lemma OAI.ContingencyTables.RootedRestartPrefix.accumulate line 23
  2. theorem OAI.ContingencyTables.RootedRestartPrefix.reference_two_warm_at line 29
  3. theorem OAI.ContingencyTables.RootedRestartPrefix.reference_next_four_warm_at line 49
  4. theorem OAI.ContingencyTables.RootedRestartPrefix.implemented_distance_prefix line 61