OAI/Combinatorics/ContingencyTables/Transport/IntegerLaw.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ContingencyTables.IntegerLaw line 13

   Source documentation

   Counts of equally likely slots. The denominator is explicit so that composition can reserve ignored bits without enumerating them.

   structure IntegerLaw (A : Type*) [Fintype A] (Q : ℕ) where
   …

2. def OAI.ContingencyTables.IntegerLaw.toRational line 23
3. def OAI.ContingencyTables.IntegerLaw.ofMass line 30
4. lemma OAI.ContingencyTables.IntegerLaw.toRational_ofMass line 41
5. def OAI.ContingencyTables.IntegerLaw.rebase line 47
6. lemma OAI.ContingencyTables.IntegerLaw.toRational_rebase line 50
7. def OAI.ContingencyTables.IntegerLaw.scale line 53
8. theorem OAI.ContingencyTables.IntegerLaw.toRational_scale line 57
9. def OAI.ContingencyTables.IntegerLaw.pi line 65
10. theorem OAI.ContingencyTables.IntegerLaw.toRational_pi line 70
11. def OAI.ContingencyTables.IntegerLaw.point line 79
12. def OAI.ContingencyTables.IntegerLaw.push line 83
13. def OAI.ContingencyTables.IntegerLaw.bind line 89
14. def OAI.ContingencyTables.IntegerLaw.product line 95
15. theorem OAI.ContingencyTables.IntegerLaw.toRational_product line 101
16. theorem OAI.ContingencyTables.IntegerLaw.toRational_push line 112
17. theorem OAI.ContingencyTables.IntegerLaw.toRational_bind line 123
18. theorem OAI.ContingencyTables.IntegerLaw.toRational_point line 137
19. def OAI.ContingencyTables.IntegerLaw.retryCount line 148
20. lemma OAI.ContingencyTables.IntegerLaw.retryCount_total line 152
21. def OAI.ContingencyTables.IntegerLaw.retry line 162
22. theorem OAI.ContingencyTables.IntegerLaw.toRational_retry line 167

    Source documentation

    First-success sums are evaluated in integers with a reserved common denominator. No division by the acceptance probability occurs.

    theorem toRational_retry (p : IntegerLaw (Option A) Q) (hQ : 0<Q)
        (fallback : A) (N : ℕ) :
        (p.retry fallback N).toRational (pow_pos hQ N)=
          retryLaw (p.toRational hQ) id fallback N := by
    …

    Mentions: OAI.ContingencyTables.IntegerLaw, OAI.ContingencyTables.IntegerLaw.toRational