OAI/Combinatorics/ContingencyTables/Transport/IndexedTableLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.IndexedTableLaw.Index line 13
2. def OAI.ContingencyTables.IndexedTableLaw.index line 15
3. def OAI.ContingencyTables.IndexedTableLaw.tableAt line 18
4. lemma OAI.ContingencyTables.IndexedTableLaw.tableAt_eq_some line 21
5. lemma OAI.ContingencyTables.IndexedTableLaw.tableAt_index line 32
6. lemma OAI.ContingencyTables.IndexedTableLaw.index_eq_iff line 36
7. def OAI.ContingencyTables.IndexedTableLaw.law line 46
8. lemma OAI.ContingencyTables.IndexedTableLaw.count_none line 50
9. lemma OAI.ContingencyTables.IndexedTableLaw.count_some line 56

   Source documentation

   Invalid completions have zero count; every valid completion has exactly the count of its unique feasible table.

   lemma count_some (htotal : ∑ i,R i=∑ j,P j) (hN : (∑ i,R i)≤N)
       (p : IntegerLaw (Option (Table R P)) Q) (k : Index m n N) :
       (law R P hN p).count (some k)=
         (tableAt R P htotal k).elim 0 (fun X => p.count (some X)) := by
   …

   Mentions: OAI.ContingencyTables.IntegerLaw, OAI.ContingencyTables.Table, OAI.ContingencyTables.IndexedTableLaw.Index, OAI.ContingencyTables.IndexedTableLaw.law, OAI.ContingencyTables.IndexedTableLaw.tableAt

10. lemma OAI.ContingencyTables.IndexedTableLaw.count_index line 65
11. theorem OAI.ContingencyTables.IndexedTableLaw.retry_count_index line 73

    Source documentation

    Embedding tables into the explicit finite candidate list commutes with every bounded first-success retry.

    theorem retry_count_index (htotal : ∑ i,R i=∑ j,P j) (hN : (∑ i,R i)≤N)
        (p : IntegerLaw (Option (Table R P)) Q) (fallback X : Table R P) (J : ℕ) :
        ((law R P hN p).retry (index R P hN fallback) J).count (index R P hN X)=
          (p.retry fallback J).count X := by
    …

    Mentions: OAI.ContingencyTables.IntegerLaw, OAI.ContingencyTables.Table, OAI.ContingencyTables.IndexedTableLaw.law, OAI.ContingencyTables.IndexedTableLaw.index