OAI/Combinatorics/ContingencyTables/Counting/CompanionEstimatorConfidence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.CompanionOracleDensity.average_fintype_irrel line 15
2. def OAI.ContingencyTables.CompanionOracleDensity.badFactor line 22
3. lemma OAI.ContingencyTables.CompanionOracleDensity.factor_failure line 29
4. theorem OAI.ContingencyTables.CompanionOracleDensity.goodEstimate_failure line 72

   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) (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.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.PublishedInputs.FiniteCheeger

5. lemma OAI.ContingencyTables.CompanionOracleDensity.innerTolerance_pos line 98
6. lemma OAI.ContingencyTables.CompanionOracleDensity.innerTolerance_lt_one line 101
7. theorem OAI.ContingencyTables.CompanionOracleDensity.estimateValue_failure line 110

   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) (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))
   …

   Mentions: OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.PublishedInputs.FiniteCheeger