OAI/Combinatorics/ContingencyTables/Machines/CachedCompletionWeights.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.DensePrograms.CompletionCache line 11
2. def OAI.ContingencyTables.DensePrograms.cachedCompletionWeight line 13
3. def OAI.ContingencyTables.DensePrograms.cachedCompletionWeightRealizer line 16
4. lemma OAI.ContingencyTables.DensePrograms.polynomial_cachedCompletionWeight line 25
5. def OAI.ContingencyTables.DensePrograms.completionWeightEntry line 34
6. def OAI.ContingencyTables.DensePrograms.completionWeightEntryRealizer line 37
7. lemma OAI.ContingencyTables.DensePrograms.polynomial_completionWeightEntry line 40
8. def OAI.ContingencyTables.DensePrograms.completionWeightInput line 43
9. def OAI.ContingencyTables.DensePrograms.completionWeightInputRealizer line 46
10. def OAI.ContingencyTables.DensePrograms.completionWeightMeasure line 50
11. lemma OAI.ContingencyTables.DensePrograms.weight_le_completionMeasure line 53
12. lemma OAI.ContingencyTables.DensePrograms.work_completionWeightInput line 58
13. def OAI.ContingencyTables.DensePrograms.completionWeights line 76
14. def OAI.ContingencyTables.DensePrograms.completionWeightsRealizer line 80
15. theorem OAI.ContingencyTables.DensePrograms.work_completionWeights line 86
16. lemma OAI.ContingencyTables.DensePrograms.cachedCompletionWeight_actual line 94
17. theorem OAI.ContingencyTables.DensePrograms.completionWeights_actual line 107

    Source documentation

    The explicit list contains every feasible table once. Each rejected free vector has zero weight; the surviving weights are the actual draw counts.

    theorem completionWeights_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 : ℕ) :
        completionWeights ((marginCode R,marginCode P),(d,h))=
          List.ofFn (fun k : Fin (((∑ i,R i)+1)^(m*n)) =>
            let o := BoxCompletion.decode R P htotal (∑ i,R i) (finFunctionFinEquiv.symm k)
    …

    Mentions: OAI.ContingencyTables.DensePrograms.completionWeights, OAI.ContingencyTables.DensePrograms.marginCode, OAI.ContingencyTables.BoxCompletion.decode