OAI/Combinatorics/ContingencyTables/Counting/CompanionFlatReturnProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.CompanionFlatReturnProgram.Input line 14
2. def OAI.ContingencyTables.CompanionFlatReturnProgram.widthInput line 16
3. def OAI.ContingencyTables.CompanionFlatReturnProgram.widthInputRealizer line 18
4. lemma OAI.ContingencyTables.CompanionFlatReturnProgram.polynomial_widthInput line 21
5. def OAI.ContingencyTables.CompanionFlatReturnProgram.width line 28
6. def OAI.ContingencyTables.CompanionFlatReturnProgram.widthRealizer line 29
7. lemma OAI.ContingencyTables.CompanionFlatReturnProgram.polynomial_width line 32
8. def OAI.ContingencyTables.CompanionFlatReturnProgram.words line 35
9. def OAI.ContingencyTables.CompanionFlatReturnProgram.wordsRealizer line 36
10. lemma OAI.ContingencyTables.CompanionFlatReturnProgram.polynomial_words line 41
11. def OAI.ContingencyTables.CompanionFlatReturnProgram.returnInput line 46
12. def OAI.ContingencyTables.CompanionFlatReturnProgram.returnInputRealizer line 47
13. lemma OAI.ContingencyTables.CompanionFlatReturnProgram.polynomial_returnInput line 49
14. def OAI.ContingencyTables.CompanionFlatReturnProgram.output line 52
15. def OAI.ContingencyTables.CompanionFlatReturnProgram.outputRealizer line 53
16. theorem OAI.ContingencyTables.CompanionFlatReturnProgram.polynomial_output line 56
17. def OAI.ContingencyTables.CompanionFlatReturnProgram.stateData line 67
18. def OAI.ContingencyTables.CompanionFlatReturnProgram.data line 76
19. lemma OAI.ContingencyTables.CompanionFlatReturnProgram.words_data line 82
20. theorem OAI.ContingencyTables.CompanionFlatReturnProgram.output_sameLaw line 101

    Source documentation

    This law includes the computed return scan, missing-return fallback, and the independent words of every step.

    theorem output_sameLaw (A : Instance (Fin m) (Fin n)) (C K j k N : ℕ)
        (hC : 0 < C) (hj : j ≤ rationalHeight A C) (hK : 1 ≤ K)
        (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=CompanionOracleDensity.binWidth A C)
        (xi : ℚ) (hxi : 0 < xi) (z : View A → ℕ)
        (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K) (degree depth : List Bool)
    …

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.RootedCatalogGrid.freeCount