OAI/Combinatorics/ContingencyTables/Transport/BoxCompletion.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.BoxCompletion.Box line 12
2. def OAI.ContingencyTables.BoxCompletion.freeValues line 14
3. def OAI.ContingencyTables.BoxCompletion.decode line 17
4. def OAI.ContingencyTables.BoxCompletion.encode line 24
5. lemma OAI.ContingencyTables.BoxCompletion.freeValues_encode line 29
6. lemma OAI.ContingencyTables.BoxCompletion.decode_encode line 35
7. theorem OAI.ContingencyTables.BoxCompletion.decode_eq_some line 50

   Source documentation

   Each feasible table occurs at exactly one enumerated free vector.

   theorem decode_eq_some {m n N : ℕ} (R : Option (Fin m) → ℕ)
       (P : Option (Fin n) → ℕ) (htotal : ∑ i,R i=∑ j,P j)
       (hN : (∑ i,R i)≤N) (z : Box m n N) (X : Table R P) :
       decode R P htotal N z=some X ↔ z=encode R P hN X := by
   …

   Mentions: OAI.ContingencyTables.BoxCompletion.Box, OAI.ContingencyTables.Table, OAI.ContingencyTables.BoxCompletion.decode, OAI.ContingencyTables.BoxCompletion.encode

8. lemma OAI.ContingencyTables.BoxCompletion.decode_elim_sum line 70
9. theorem OAI.ContingencyTables.BoxCompletion.sum_decode line 76

   Source documentation

   Summing over candidate completions counts each feasible table once, and gives zero weight to every rejected completion.

   theorem sum_decode {m n N : ℕ} (R : Option (Fin m) → ℕ)
       (P : Option (Fin n) → ℕ) (htotal : ∑ i,R i=∑ j,P j)
       (hN : (∑ i,R i)≤N) (w : Table R P → ℕ) :
       (∑ z : Box m n N,(decode R P htotal N z).elim 0 w)=∑ X,w X := by
   …

   Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.BoxCompletion.Box, OAI.ContingencyTables.BoxCompletion.decode

10. theorem OAI.ContingencyTables.BoxCompletion.acceptCompletion_eq line 89

    Source documentation

    The existing executable acceptance test returns the same optional table as the finite enumeration used in the counting proof.

    theorem acceptCompletion_eq {m n N : ℕ} (R : Option (Fin m) → ℕ)
        (P : Option (Fin n) → ℕ) (htotal : ∑ i,R i=∑ j,P j) (z : Box m n N) :
        acceptCompletion ((marginCode R,marginCode P),
          matrixCode (fun i j => freeValues z (i,j)))=
          (decode R P htotal N z).map tableOutput := by
    …

    Mentions: OAI.ContingencyTables.BoxCompletion.Box, OAI.ContingencyTables.BoxCompletion.freeValues, OAI.ContingencyTables.BoxCompletion.decode