OAI/Combinatorics/ContingencyTables/Counting/CompanionOracleAcceptance.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.CompanionOracleAcceptance.ratio_linear_bounds line 16
2. lemma OAI.ContingencyTables.CompanionOracleAcceptance.min_one_stability line 44
3. def OAI.ContingencyTables.CompanionOracleAcceptance.evaluatedWeight line 61
4. def OAI.ContingencyTables.CompanionOracleAcceptance.targetWeight line 67
5. lemma OAI.ContingencyTables.CompanionOracleAcceptance.targetWeight_eq line 71
6. lemma OAI.ContingencyTables.CompanionOracleAcceptance.multiplier_positive line 77
7. lemma OAI.ContingencyTables.CompanionOracleAcceptance.targetWeight_positive line 84
8. def OAI.ContingencyTables.CompanionOracleAcceptance.acceptance line 89
9. def OAI.ContingencyTables.CompanionOracleAcceptance.targetAcceptance line 97
10. lemma OAI.ContingencyTables.CompanionOracleAcceptance.targetAcceptance_eq line 100
11. lemma OAI.ContingencyTables.CompanionOracleAcceptance.evaluatedWeight_bounds line 105
12. theorem OAI.ContingencyTables.CompanionOracleAcceptance.acceptance_error line 120

    Source documentation

    Relative errors in both weight calls cause an absolute acceptance error at most four times the call tolerance, even across clipping at 1.

    theorem acceptance_error (A : Instance I J) (C K j : ℕ)
        (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (xi : ℚ) (hx0 : 0 ≤ xi) (hx1 : xi ≤ 1/4)
        (v : Grid (I := Fin (dimension A)) K) (w : Pair A → Pair A → ℚ)
    …

13. lemma OAI.ContingencyTables.CompanionOracleAcceptance.acceptance_bounds line 140
14. lemma OAI.ContingencyTables.CompanionOracleAcceptance.targetAcceptance_bounds line 154
15. theorem OAI.ContingencyTables.CompanionOracleAcceptance.average_acceptance_error line 163

    Source documentation

    This is the rounded acceptance probability of the implemented decision, averaged over its two fresh independent weight-query words.

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

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