OAI/Combinatorics/ContingencyTables/Machines/FiniteWordRejection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Repeated rejection implemented by one finite independent Boolean array

  1. theorem OAI.ContingencyTables.FirstSuccess.retryLaw_map line 15
  2. def OAI.ContingencyTables.FirstSuccess.wordRetry line 31
  3. def OAI.ContingencyTables.FirstSuccess.wordRetryLaw line 36
  4. theorem OAI.ContingencyTables.FirstSuccess.wordRetryLaw_eq line 41

    Source documentation

    The first successful output is computed from an actual fixed Boolean array; unused suffix words do not change its distribution.

    theorem wordRetryLaw_eq {k : ℕ} (f : (Fin k → Bool) → Option α) (fallback : α) (n : ℕ) :
    wordRetryLaw f fallback n = retryLaw (uniformLaw (α := Fin k → Bool)) f fallback n := by
…

    Mentions: OAI.ContingencyTables.FirstSuccess.wordRetryLaw, OAI.ContingencyTables.FirstSuccess.retryLaw, OAI.ContingencyTables.FirstSuccess.uniformLaw