OAI/Combinatorics/ContingencyTables/Rooted/RootedEstimatorWordLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.RootedEstimatorWordProgram.scheduledContext line 18
2. def OAI.ContingencyTables.RootedEstimatorWordProgram.scheduledEquiv line 24
3. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.scheduledWordWidth line 34
4. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.oracleTime_positive line 46
5. theorem OAI.ContingencyTables.RootedEstimatorWordProgram.scheduledWidth_positive line 59
6. theorem OAI.ContingencyTables.RootedEstimatorWordProgram.prepare_scheduled line 81

   Source documentation

   Parsing the one flat word produces precisely the sample inputs used in the independent estimator experiment.

   theorem prepare_scheduled (A : Instance (Fin m) (Fin n)) (C K j : ℕ)
       (hC : 0 < C) (hK : 1 ≤ K) (delta failure : ℚ) (hd : 0 < delta) (hf : 0 < failure)
       (z : View A → ℕ) (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K)
   …

   Mentions: OAI.ContingencyTables.RootedCatalogGrid.freeCount

7. theorem OAI.ContingencyTables.RootedEstimatorWordProgram.output_scheduled line 127
8. theorem OAI.ContingencyTables.RootedEstimatorWordProgram.sameLaw_estimateValue line 143
9. theorem OAI.ContingencyTables.RootedEstimatorWordProgram.sameLaw_word line 171
10. theorem OAI.ContingencyTables.RootedEstimatorWordProgram.output_range line 192
11. theorem OAI.ContingencyTables.RootedEstimatorWordProgram.output_failure line 212

    Source documentation

    The actual polynomial list program, on its prescribed finite word, inherits the proved relative-error bound of the complete weight oracle.

    theorem output_failure (A : Instance (Fin m) (Fin n)) (C K j : ℕ)
        (hC : 0 < C) (hj : j ≤ rationalHeight A C) (hK : 1 ≤ K)
        (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=CompanionOracleDensity.binWidth A C)
        (epsilon failure : ℚ) (he0 : 0 < epsilon) (he1 : epsilon < 1) (hf : 0 < failure)
        (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
        (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K) (degree depth : List Bool)
    …

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