OAI/Combinatorics/ContingencyTables/Rooted/RootedWeightOracle.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.RootedWeightOracle.weight_source line 20
2. def OAI.ContingencyTables.RootedWeightOracle.evaluate line 31
3. def OAI.ContingencyTables.RootedWeightOracle.accurateCall line 38

   Source documentation

   The relative-accuracy event for the rational labelled-weight estimate.

   def accurateCall (A : Instance I J) (R : RootedCompletion.Selection A.T) (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))
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection

4. lemma OAI.ContingencyTables.RootedWeightOracle.evaluate_positive line 45
5. theorem OAI.ContingencyTables.RootedWeightOracle.evaluate_success line 59

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