OAI/Combinatorics/ContingencyTables/Machines/OffsetCountProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.OffsetCountPrograms.ceilQuotient line 11
2. def OAI.ContingencyTables.OffsetCountPrograms.ceilQuotientRealizer line 13
3. lemma OAI.ContingencyTables.OffsetCountPrograms.polynomial_ceilQuotient line 18
4. lemma OAI.ContingencyTables.OffsetCountPrograms.ceilQuotient_eq line 25
5. abbrev OAI.ContingencyTables.OffsetCountPrograms.Input line 40
6. def OAI.ContingencyTables.OffsetCountPrograms.endpoint line 42
7. def OAI.ContingencyTables.OffsetCountPrograms.endpointRealizer line 44
8. lemma OAI.ContingencyTables.OffsetCountPrograms.polynomial_endpoint line 49
9. def OAI.ContingencyTables.OffsetCountPrograms.offsetCount line 55
10. def OAI.ContingencyTables.OffsetCountPrograms.offsetCountRealizer line 57
11. lemma OAI.ContingencyTables.OffsetCountPrograms.polynomial_offsetCount line 62
12. lemma OAI.ContingencyTables.OffsetCountPrograms.endpoint_eq line 68
13. theorem OAI.ContingencyTables.OffsetCountPrograms.offsetCount_eq line 75

    Source documentation

    Only two ceiling divisions are required, regardless of the number of random words whose probability is being counted.

    theorem offsetCount_eq (M Q β : ℕ) (hM : 0<M) (hQ : 0<Q) (hβ : β<M) :
        offsetCount ((M,Q),β)=(FairBits.fiber M Q β).card := by
    …

    Mentions: OAI.ContingencyTables.OffsetCountPrograms.offsetCount, OAI.ContingencyTables.FairBits.fiber

14. theorem OAI.ContingencyTables.OffsetCountPrograms.scaledLaw_mass line 79