OAI/Combinatorics/ContingencyTables/Rooted/RootedPhaseOracleError.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.RootedPhaseWords.accurateCalls line 21
2. lemma OAI.ContingencyTables.RootedPhaseWords.accurateCall_failure line 28
3. lemma OAI.ContingencyTables.RootedPhaseWords.pairedCalls_failure line 40
4. theorem OAI.ContingencyTables.RootedPhaseWords.accurateCalls_failure line 59

   Source documentation

   The calls use independent actual finite words even for a fixed, arbitrary sequence of observed states. No sampling assumption on that sequence is required for this oracle-error estimate.

   theorem accurateCalls_failure (A : Instance I J) (R : RootedCompletion.Selection A.T) (C : ℕ) (hC : 0 < C) (K j N : ℕ)
       (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=binWidth A C)
       (hj : j+1 ≤ 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

5. def OAI.ContingencyTables.RootedPhaseWords.exactObservedRatio line 105

   Source documentation

   The exact empirical ratio written as the plain-state sum divided by its integer plain-state population.

   def exactObservedRatio (A : Instance I J) (R : RootedCompletion.Selection A.T) (j N : ℕ)
       (states : Fin N → Set (Labels A×Bool)) : ℝ :=
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection

6. lemma OAI.ContingencyTables.RootedPhaseWords.indicator_list_sum_real line 110
7. lemma OAI.ContingencyTables.RootedPhaseWords.exactObservedRatio_eq line 116
8. lemma OAI.ContingencyTables.RootedPhaseWords.ratio_exponential_bounds line 130
9. lemma OAI.ContingencyTables.RootedPhaseWords.observedTerm_bounds line 151
10. lemma OAI.ContingencyTables.RootedPhaseWords.exactObservedRatio_positive line 172
11. theorem OAI.ContingencyTables.RootedPhaseWords.observedRatio_bounds line 196

    Source documentation

    Relative errors of all fresh calls remain bounded after averaging the state ratios. The number of observations does not enlarge this deterministic multiplicative error.

    theorem observedRatio_bounds (A : Instance I J) (R : RootedCompletion.Selection A.T) (C K j N : ℕ)
        (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) (states : Fin N → Set (Labels A×Bool))
    …

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection

12. theorem OAI.ContingencyTables.RootedPhaseWords.observedRatio_log_error line 218