OAI/Combinatorics/ContingencyTables/Transport/CanonicalDrawTabulation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.DensePrograms.canonicalCountInput line 11
2. def OAI.ContingencyTables.DensePrograms.canonicalCountInputRealizer line 15
3. lemma OAI.ContingencyTables.DensePrograms.polynomial_canonicalCountInput line 25
4. def OAI.ContingencyTables.DensePrograms.canonicalDrawCounts line 38
5. def OAI.ContingencyTables.DensePrograms.canonicalDrawCountsRealizer line 41
6. def OAI.ContingencyTables.DensePrograms.canonicalTabulationMeasure line 46
7. theorem OAI.ContingencyTables.DensePrograms.work_canonicalDrawCounts line 52
8. def OAI.ContingencyTables.DensePrograms.canonicalTableIndex line 71

   Source documentation

   The lookup index uses exactly the same two swaps as the sampler.

   def canonicalTableIndex (z : CanonicalParameters×MatrixCode) : ℕ :=
   …

   Mentions: OAI.ContingencyTables.DensePrograms.CanonicalParameters, OAI.ContingencyTables.DensePrograms.MatrixCode

9. def OAI.ContingencyTables.DensePrograms.canonicalTableIndexRealizer line 74
10. lemma OAI.ContingencyTables.DensePrograms.polynomial_canonicalTableIndex line 84
11. lemma OAI.ContingencyTables.DensePrograms.canonicalCountInput_code line 94
12. lemma OAI.ContingencyTables.DensePrograms.canonicalTableIndex_code line 105
13. theorem OAI.ContingencyTables.DensePrograms.canonicalDrawCounts_at line 120

    Source documentation

    The cached numerator is the count at the transported table, including all fallback words of the actual normalized dense program.

    theorem canonicalDrawCounts_at {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 : ℕ) (X : Table R P) :
        (canonicalDrawCounts ((marginCode R,marginCode P),(d,h))).getD
          (canonicalTableIndex (((marginCode R,marginCode P),(d,h)),tableOutput X)) 0=
        (denseDrawCounts (normalizedMargin R) (normalizedMargin P) d hd
          (normalizedMargin_lower R _ hR) (normalizedMargin_lower P _ hP)
          finProdFinEquiv (by rw [normalizedMargin_total,normalizedMargin_total]; exact htotal) h
          (canonicalOrigin (m*n) d (by omega))
          (tableReindex (indexPermutation (marginPosition R))
            (indexPermutation (marginPosition P)) R P (canonicalFallback R P htotal))).count
    …

    Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.DensePrograms.canonicalDrawCounts, OAI.ContingencyTables.DensePrograms.marginCode, OAI.ContingencyTables.DensePrograms.canonicalTableIndex, OAI.ContingencyTables.DensePrograms.tableOutput, OAI.ContingencyTables.DensePrograms.normalizedMargin, OAI.ContingencyTables.DensePrograms.normalizedMargin_lower, OAI.ContingencyTables.DensePrograms.normalizedMargin_total, OAI.ContingencyTables.DensePrograms.canonicalOrigin, OAI.ContingencyTables.tableReindex, OAI.ContingencyTables.DensePrograms.indexPermutation, OAI.ContingencyTables.DensePrograms.marginPosition, OAI.ContingencyTables.DensePrograms.canonicalFallback