OAI/Combinatorics/ContingencyTables/Sampling/OriginalBoxLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.OriginalBoxLaw.tableAt_index line 14
2. lemma OAI.ContingencyTables.OriginalBoxLaw.index_eq_iff line 18
3. def OAI.ContingencyTables.OriginalBoxLaw.law line 28
4. lemma OAI.ContingencyTables.OriginalBoxLaw.count_none line 32
5. lemma OAI.ContingencyTables.OriginalBoxLaw.count_some line 38

   Source documentation

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

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

   Mentions: OAI.ContingencyTables.IntegerLaw, OAI.ContingencyTables.Table, OAI.ContingencyTables.OriginalBoxLaw.law

6. lemma OAI.ContingencyTables.OriginalBoxLaw.count_index line 47
7. theorem OAI.ContingencyTables.OriginalBoxLaw.retry_count_index line 55

   Source documentation

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

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

   Mentions: OAI.ContingencyTables.IntegerLaw, OAI.ContingencyTables.Table, OAI.ContingencyTables.OriginalBoxLaw.law

8. lemma OAI.ContingencyTables.OriginalBoxLaw.retry_count_some line 67

   Source documentation

   A retry keeps every invalid finite-box entry at zero.

   lemma retry_count_some (hN : (∑ i,r i)≤N)
       (p : IntegerLaw (Option (Table r c)) Q) (fallback : Table r c) (J : ℕ)
       (k : Index m n N) :
       ((law r c hN p).retry (index r c hN fallback) J).count k=
         (tableAt r c k).elim 0 (fun T => (p.retry fallback J).count T) := by
   …

   Mentions: OAI.ContingencyTables.IntegerLaw, OAI.ContingencyTables.Table, OAI.ContingencyTables.OriginalBoxLaw.law