OAI/Combinatorics/ContingencyTables/Machines/FiniteWordWalk.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact laws of a walk driven by independent fixed-length Boolean words

  1. def OAI.ContingencyTables.FirstSuccess.uniformMapMass line 17
  2. theorem OAI.ContingencyTables.FirstSuccess.uniformMapMass_equiv line 21
  3. theorem OAI.ContingencyTables.FirstSuccess.finite_fiber_sum line 28
  4. theorem OAI.ContingencyTables.FirstSuccess.uniformMapMass_prod line 34
  5. theorem OAI.ContingencyTables.FirstSuccess.uniform_map_mass line 43
  6. def OAI.ContingencyTables.FirstSuccess.wordWalk line 50
  7. def OAI.ContingencyTables.FirstSuccess.wordWalkLaw line 55
  8. theorem OAI.ContingencyTables.FirstSuccess.wordWalkLaw_eq line 60

    Source documentation

    A uniform finite Boolean array realizes the independent transition-law composition, with no random-length source or conditioning.

    theorem wordWalkLaw_eq {k : ℕ} (step : α → (Fin k → Bool) → α) (a : α) (n : ℕ) :
    wordWalkLaw step a n = walkLaw (fun s => mapLaw (uniformLaw (α := Fin k → Bool)) (step s)) a n := by
…

    Mentions: OAI.ContingencyTables.FirstSuccess.wordWalkLaw, OAI.ContingencyTables.FirstSuccess.walkLaw, OAI.ContingencyTables.FirstSuccess.mapLaw, OAI.ContingencyTables.FirstSuccess.uniformLaw