OAI/Combinatorics/ContingencyTables/Counting/CompanionInitializedRestartSemantics.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionInitializedRestartProgram.data line 17
2. lemma OAI.ContingencyTables.CompanionInitializedRestartProgram.stages_data line 25
3. lemma OAI.ContingencyTables.CompanionInitializedRestartProgram.initialWidth_data line 44
4. theorem OAI.ContingencyTables.CompanionInitializedRestartProgram.output_split line 55

   Source documentation

   Exact physical splitting: the initializer sees the first block, the restart loop sees the remaining block, and all markers are fixed.

   theorem output_split (A : Instance (Fin m) (Fin n)) (C K H T N R L j s : ℕ)
       (epsilon : TreeFraction.Fraction) (z : View A → ℕ)
       (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K)
   …

   Mentions: OAI.ContingencyTables.RootedCatalogGrid.freeCount