OAI/Combinatorics/ContingencyTables/Dense/DenseIndexedCounts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.DensePrograms.candidateCounts_indexed line 14
2. theorem OAI.ContingencyTables.DensePrograms.denseRetryVector_actual line 38

   Source documentation

   Full retry numerators are obtained by the polynomial binary vector recurrence, after the accepted-trial vector has been tabulated once.

   theorem denseRetryVector_actual {m n d : ℕ} (R : Option (Fin m) → ℕ)
       (P : Option (Fin n) → ℕ) (hd : 14≤d) (hq : m*n≤d)
       (hR : ∀ i,d^12≤R i) (hP : ∀ j,d^12≤P j) (htotal : ∑ i,R i=∑ j,P j)
       (h : ℕ) (cap xs : List Bool)
       (hcap : ∀ j : Fin (m*n),FairBits.offsetBitLength
         (integerWidth R P d (finProdFinEquiv.symm j)) h d≤cap.length)
       (fallback : Table R P) :
       VectorRetryPrograms.counts ((xs,2^denseTrialBits R P d finProdFinEquiv h),
         (candidateCounts ((tabulateDenseWalk ((marginCode R,marginCode P),(d,h)),cap),
           ((marginCode R,marginCode P),(d,h))),
           (IndexedTableLaw.index R P (le_refl (∑ i,R i)) fallback).val))=
       List.ofFn (((IndexedTableLaw.law R P (le_refl (∑ i,R i))
   …

   Mentions: OAI.ContingencyTables.FairBits.offsetBitLength, OAI.ContingencyTables.Table, OAI.ContingencyTables.VectorRetryPrograms.counts, OAI.ContingencyTables.DensePrograms.candidateCounts, OAI.ContingencyTables.DensePrograms.tabulateDenseWalk, OAI.ContingencyTables.DensePrograms.marginCode, OAI.ContingencyTables.IndexedTableLaw.index, OAI.ContingencyTables.IndexedTableLaw.law