OAI/Combinatorics/ContingencyTables/Dense/DenseSuppliedFallback.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.DensePrograms.SuppliedTabulation line 11
2. def OAI.ContingencyTables.DensePrograms.replaceVectorFallback line 13
3. def OAI.ContingencyTables.DensePrograms.replaceVectorFallbackRealizer line 16
4. lemma OAI.ContingencyTables.DensePrograms.polynomial_replaceVectorFallback line 19
5. def OAI.ContingencyTables.DensePrograms.suppliedVectorInput line 24
6. def OAI.ContingencyTables.DensePrograms.suppliedVectorInputRealizer line 27
7. def OAI.ContingencyTables.DensePrograms.suppliedTabulationMeasure line 36
8. lemma OAI.ContingencyTables.DensePrograms.work_suppliedVectorInput line 38
9. def OAI.ContingencyTables.DensePrograms.suppliedDrawCounts line 57
10. def OAI.ContingencyTables.DensePrograms.suppliedDrawCountsRealizer line 60
11. theorem OAI.ContingencyTables.DensePrograms.work_suppliedDrawCounts line 63
12. theorem OAI.ContingencyTables.DensePrograms.suppliedDrawCounts_actual line 79

    Source documentation

    The fallback is transported by the caller's normalization, rather than being recomputed in the normalized margin order.

    theorem suppliedDrawCounts_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 : ℕ) (fallback : Table R P) :
        suppliedDrawCounts (((marginCode R,marginCode P),(d,h)),tableOutput fallback)=
          List.ofFn (((IndexedTableLaw.law R P (le_refl (∑ i,R i))
            ((denseTrialCounts R P d hd hR hP finProdFinEquiv h
              (canonicalOrigin (m*n) d (by omega))).push
                (trialSuccess R P d finProdFinEquiv htotal))).retry
            (IndexedTableLaw.index R P (le_refl (∑ i,R i)) fallback) (d^4*(h+1))).count) := by
    …

    Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.DensePrograms.suppliedDrawCounts, OAI.ContingencyTables.DensePrograms.marginCode, OAI.ContingencyTables.DensePrograms.tableOutput, OAI.ContingencyTables.IndexedTableLaw.law, OAI.ContingencyTables.DensePrograms.canonicalOrigin, OAI.ContingencyTables.IndexedTableLaw.index

13. theorem OAI.ContingencyTables.DensePrograms.suppliedDrawCounts_at line 111