OAI/Combinatorics/ContingencyTables/Machines/CachedStepCount.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.ProfilePrograms.DecisionQuery line 16
2. def OAI.ContingencyTables.ProfilePrograms.decisionWeight line 20

   Source documentation

   A rejected box entry contributes zero. A valid completion contributes its cached integer multiplicity precisely when it reaches the target.

   def decisionWeight (z : DecisionQuery×(Option MatrixCode×ℕ)) : ℕ :=
   …

   Mentions: OAI.ContingencyTables.ProfilePrograms.DecisionQuery

3. def OAI.ContingencyTables.ProfilePrograms.decisionWeightRealizer line 23
4. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_decisionWeight line 38
5. def OAI.ContingencyTables.ProfilePrograms.decisionWeightSum line 54
6. def OAI.ContingencyTables.ProfilePrograms.decisionWeightSumRealizer line 57
7. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_decisionWeightSum line 60
8. lemma OAI.ContingencyTables.DensePrograms.sum_completionWeights line 70

   Source documentation

   Free-box enumeration sums each feasible table's weight once.

   lemma sum_completionWeights {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 : ℕ) (w : MatrixCode → ℕ) :
       ((completionWeights ((marginCode R,marginCode P),(d,h))).map
         (fun z => z.1.elim 0 (fun X => z.2*w X))).sum=
         ∑ X : Table R P,(canonicalCounts R P hd hR hP htotal h).count X*w (tableOutput X) := by
   …

   Mentions: OAI.ContingencyTables.DensePrograms.MatrixCode, OAI.ContingencyTables.DensePrograms.completionWeights, OAI.ContingencyTables.DensePrograms.marginCode, OAI.ContingencyTables.Table, OAI.ContingencyTables.DensePrograms.canonicalCounts, OAI.ContingencyTables.DensePrograms.tableOutput

9. lemma OAI.ContingencyTables.SmallGraphProfiles.decisionWeightSum_actual line 114