OAI/Combinatorics/ContingencyTables/Machines/FiniteWordPadding.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.FirstSuccess.mapLaw_product_fst line 16
2. def OAI.ContingencyTables.FirstSuccess.prefixWord line 29
3. def OAI.ContingencyTables.FirstSuccess.paddingWordEquiv line 32
4. lemma OAI.ContingencyTables.FirstSuccess.paddingWordEquiv_fst line 37
5. theorem OAI.ContingencyTables.FirstSuccess.prefixWord_uniform line 47

   Source documentation

   Taking the needed prefix of a larger uniform word preserves the exact law, so unused bits can be reserved even after the current state is known.

   theorem prefixWord_uniform {k N : ℕ} (hk : k ≤ N) :
       mapLaw (uniformLaw (α := Fin N → Bool)) (prefixWord hk)=uniformLaw (α := Fin k → Bool) := by
   …

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

6. theorem OAI.ContingencyTables.FirstSuccess.padded_draw_law line 58

   Source documentation

   An arbitrary finite draw keeps its law when padded to the common bound; this applies separately at every state of an adaptive walk.

   theorem padded_draw_law {k N : ℕ} (hk : k ≤ N) (draw : (Fin k → Bool) → Y) :
       mapLaw (uniformLaw (α := Fin N → Bool)) (fun bits => draw (prefixWord hk bits))=
   …

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