OAI/Combinatorics/ContingencyTables/Machines/FiniteWordJointPadding.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.FiniteObservableTransport.SameLaw.append_joint line 11
2. theorem OAI.ContingencyTables.FiniteObservableTransport.restart_append_joint_sameLaw line 27
3. theorem OAI.ContingencyTables.FiniteObservableTransport.nested_word_joint line 50

   Source documentation

   Flattening the first two independent blocks preserves their joint law with the untouched third block.

   theorem nested_word_joint {Z : Type*} (a b t : ℕ)
       (f : (Fin a → Bool) → (Fin b → Bool) → Z) :
       SameLaw (fun bits : Fin (a+(b+t)) → Bool =>
         (f (splitWordEquiv a (b+t) bits).1
           (splitWordEquiv b t (splitWordEquiv a (b+t) bits).2).1,
           (splitWordEquiv b t (splitWordEquiv a (b+t) bits).2).2))
         (fun bits : (Fin (a+b) → Bool)×(Fin t → Bool) =>
           (f (splitWordEquiv a b bits.1).1 (splitWordEquiv a b bits.1).2,bits.2)) := by
   …

   Mentions: OAI.ContingencyTables.FiniteObservableTransport.SameLaw