OAI/Combinatorics/ContingencyTables/Machines/FiniteVaryingWordWalk.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Independent words for successive draws with varying widths

  1. abbrev OAI.ContingencyTables.FirstSuccess.VaryingWords line 15
  2. def OAI.ContingencyTables.FirstSuccess.varyingWalk line 18
  3. def OAI.ContingencyTables.FirstSuccess.varyingLaw line 24
  4. theorem OAI.ContingencyTables.FirstSuccess.varyingWalk_law line 31
  5. lemma OAI.ContingencyTables.FirstSuccess.bindLaw_associative line 66
  6. theorem OAI.ContingencyTables.FirstSuccess.varyingLaw_start line 73
  7. def OAI.ContingencyTables.FirstSuccess.varyingWordEquiv line 89
  8. theorem OAI.ContingencyTables.FirstSuccess.flatVaryingWalk_law line 96

    Source documentation

    The flattened word consumes exactly the sum of the successive widths, including unused bits on any branch of the deterministic draws.

    theorem flatVaryingWalk_law (width : ℕ → ℕ)
    (step : (i : ℕ) → X → (Fin (width i) → Bool) → X) (x : X) (n : ℕ) :
    mapLaw (uniformLaw (α := Fin (∑ i : Fin n,width i.val) → Bool))
…

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