OAI/Combinatorics/ContingencyTables/Counting/CompanionWeightOracle.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionWeightOracle.profile line 18
2. lemma OAI.ContingencyTables.CompanionWeightOracle.profile_inBox line 21
3. def OAI.ContingencyTables.CompanionWeightOracle.factorialNumerator line 26
4. def OAI.ContingencyTables.CompanionWeightOracle.factorialDenominator line 29
5. def OAI.ContingencyTables.CompanionWeightOracle.factorialRatio line 32
6. lemma OAI.ContingencyTables.CompanionWeightOracle.factorialRatio_positive line 35
7. lemma OAI.ContingencyTables.CompanionWeightOracle.factorialRatio_cast line 40
8. theorem OAI.ContingencyTables.CompanionWeightOracle.weight_source line 47
9. abbrev OAI.ContingencyTables.CompanionWeightOracle.WeightWord line 58
10. def OAI.ContingencyTables.CompanionWeightOracle.evaluate line 61
11. def OAI.ContingencyTables.CompanionWeightOracle.accurateCall line 69

    Source documentation

    The relative-accuracy event describes the weight evaluator at each labelled state.

    def accurateCall (A : Instance I J) (C K j : ℕ)
        (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (xi : ℚ)
        (v : Grid (I := Fin (dimension A)) K) (S : Set (Labels A×Bool))
    …

12. lemma OAI.ContingencyTables.CompanionWeightOracle.evaluate_positive line 76
13. theorem OAI.ContingencyTables.CompanionWeightOracle.evaluate_success line 90

    Source documentation

    Every query at the actual labelled state uses a fresh bounded word. Only PL and finite Cheeger remain in the evaluation guarantee.

    theorem evaluate_success (A : Instance I J) (C : ℕ) (hC : 0 < C) (K : ℕ)
        (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=binWidth A C)
        (j : ℕ) (hj : j ≤ rationalHeight A C) (xi : ℚ) (hx0 : 0 < xi) (hx1 : xi < 1)
        (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
        (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
    …

    Mentions: OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger