OAI/Combinatorics/ContingencyTables/Dense/DenseTransitionCounts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.GridBoundary.denseTransitionCount line 17
2. lemma OAI.ContingencyTables.GridBoundary.denseTransitionCount_total line 23
3. lemma OAI.ContingencyTables.GridBoundary.denseTransitionCount_off_diagonal line 33
4. theorem OAI.ContingencyTables.GridBoundary.denseTransitionCount_kernel line 47

   Source documentation

   The tabulated integer matrix is the actual Boolean step law, including all unused proposal codes and all rejections.

   theorem denseTransitionCount_kernel (R : Option I → ℕ) (P : Option J → ℕ) (d : ℕ)
       (e : I × J ≃ Fin q) (a : Grid (I := Fin q) (4*d^8)) :
   …

   Mentions: OAI.ContingencyTables.GridBoundary.Grid

5. theorem OAI.ContingencyTables.GridBoundary.denseWalkCount_mass line 67

   Source documentation

   Matrix propagation tabulates the complete adaptive bin walk with one integer per bin; the precision affects integer lengths, not the number of bins enumerated.

   theorem denseWalkCount_mass (R : Option I → ℕ) (P : Option J → ℕ) (d : ℕ)
       (e : I × J ≃ Fin q) (a b : Grid (I := Fin q) (4*d^8)) (N : ℕ) :
   …

   Mentions: OAI.ContingencyTables.GridBoundary.Grid