OAI/Combinatorics/ContingencyTables/Counting/CompanionRestartSemantics.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionRestartProgram.widthAt line 11
2. lemma OAI.ContingencyTables.CompanionRestartProgram.widths_ofFn line 13
3. lemma OAI.ContingencyTables.CompanionRestartProgram.stageWord_ofFn line 21
4. def OAI.ContingencyTables.CompanionRestartProgram.detachedStep line 30
5. lemma OAI.ContingencyTables.CompanionRestartProgram.next_detached line 35
6. lemma OAI.ContingencyTables.CompanionRestartProgram.walk_eq line 39
7. lemma OAI.ContingencyTables.CompanionRestartProgram.fold_range_varying line 47
8. theorem OAI.ContingencyTables.CompanionRestartProgram.output_varyingWalk line 63

   Source documentation

   The bounded list program consumes exactly its independent stage blocks. No assumption about the encoded states is needed here.

   theorem output_varyingWalk (base : List Stage×List ℕ)
       (bits : Fin (∑ i : Fin base.1.length,widthAt base i.val) → Bool) :
       output (base,List.ofFn bits)=
         varyingWalk (widthAt base)
           (fun i code word => detachedStep base i code (List.ofFn word))
           base.2 base.1.length (varyingWordEquiv (widthAt base) base.1.length bits) := by
   …

   Mentions: OAI.ContingencyTables.CompanionRestartProgram.Stage, OAI.ContingencyTables.CompanionRestartProgram.widthAt, OAI.ContingencyTables.CompanionRestartProgram.output, OAI.ContingencyTables.CompanionRestartProgram.detachedStep

9. theorem OAI.ContingencyTables.CompanionRestartProgram.output_sameLaw line 81

   Source documentation

   Conditional laws compose across the actual disjoint variable-width blocks, even when the source and encoded state spaces have different sizes.

   theorem output_sameLaw {Z : Type*} (base : List Stage×List ℕ) (v : ℕ → ℕ)
       (G : (i : ℕ) → Z → (Fin (v i) → Bool) → Z) (e : Z → List ℕ)
       (z : Z) (hz : base.2=e z)
       (h : ∀ i,i < base.1.length → ∀ s,SameLaw
         (fun bits : Fin (widthAt base i) → Bool => detachedStep base i (e s) (List.ofFn bits))
         (fun bits => e (G i s bits))) :
       SameLaw (fun bits : Fin (∑ i : Fin base.1.length,widthAt base i.val) → Bool =>
         output (base,List.ofFn bits))
         (fun bits : Fin (∑ i : Fin base.1.length,v i.val) → Bool =>
           e (varyingWalk v G z base.1.length (varyingWordEquiv v base.1.length bits))) := by
   …

   Mentions: OAI.ContingencyTables.CompanionRestartProgram.Stage, OAI.ContingencyTables.CompanionRestartProgram.widthAt, OAI.ContingencyTables.CompanionRestartProgram.detachedStep, OAI.ContingencyTables.CompanionRestartProgram.output