RootedEstimatorConfidence.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Confidence of the complete bounded-word weight estimator

def OAI.ContingencyTables.RootedOracleDensity.badFactor line 19
lemma OAI.ContingencyTables.RootedOracleDensity.factor_failure line 26

theorem OAI.ContingencyTables.RootedOracleDensity.goodEstimate_failure line 69

Source documentation

All ratio and correction block failures share one explicit budget. The statement concerns the actual bounded Boolean experiment.

theorem goodEstimate_failure (A : Instance I J) (R : RootedCompletion.Selection A.T) (C : ℕ) (hC : 0 < C) (z : View A → ℕ)
    (hz : BalancedBox.InBox (bounds A) z) (K : ℕ) (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W)
    (hB : (K:ℝ)=binWidth A C) (j : ℕ) (hj : j ≤ rationalHeight A C)
    (delta failure : ℚ) (hd0 : 0 < delta) (hd1 : delta < 1) (hf : 0 < failure)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
…

Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger

theorem OAI.ContingencyTables.RootedOracleDensity.estimateValue_failure line 97

Source documentation

A concrete rational estimator with bounded independent Boolean input has the required relative-error guarantee for the original h-value.

theorem estimateValue_failure (A : Instance I J) (R : RootedCompletion.Selection A.T) (C : ℕ) (hC : 0 < C) (z : View A → ℕ)
    (hz : BalancedBox.InBox (bounds A) z) (K : ℕ) (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W)
    (hB : (K:ℝ)=binWidth A C) (j : ℕ) (hj : j ≤ rationalHeight A C)
    (epsilon failure : ℚ) (he0 : 0 < epsilon) (he1 : epsilon < 1) (hf : 0 < failure)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
…