OAI/Combinatorics/ContingencyTables/Rooted/RootedOracleAcceptance.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.RootedOracleAcceptance.ratio_linear_bounds line 18
2. lemma OAI.ContingencyTables.RootedOracleAcceptance.min_one_stability line 46
3. def OAI.ContingencyTables.RootedOracleAcceptance.evaluatedWeight line 63
4. def OAI.ContingencyTables.RootedOracleAcceptance.targetWeight line 69
5. lemma OAI.ContingencyTables.RootedOracleAcceptance.targetWeight_eq line 73
6. lemma OAI.ContingencyTables.RootedOracleAcceptance.multiplier_positive line 79
7. lemma OAI.ContingencyTables.RootedOracleAcceptance.targetWeight_positive line 86
8. def OAI.ContingencyTables.RootedOracleAcceptance.acceptance line 91
9. def OAI.ContingencyTables.RootedOracleAcceptance.targetAcceptance line 99
10. lemma OAI.ContingencyTables.RootedOracleAcceptance.targetAcceptance_eq line 102
11. lemma OAI.ContingencyTables.RootedOracleAcceptance.evaluatedWeight_bounds line 107
12. theorem OAI.ContingencyTables.RootedOracleAcceptance.acceptance_error line 122

    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) (R : RootedCompletion.Selection A.T) (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 → ℚ)
    …

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection

13. lemma OAI.ContingencyTables.RootedOracleAcceptance.acceptance_bounds line 142
14. lemma OAI.ContingencyTables.RootedOracleAcceptance.targetAcceptance_bounds line 156
15. theorem OAI.ContingencyTables.RootedOracleAcceptance.average_acceptance_error line 165

    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) (R : RootedCompletion.Selection A.T) (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.RootedCompletion.Selection, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger