OAI/Combinatorics/ContingencyTables/Counting/CompanionEstimatorRange.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalAverage_bounds line 17
2. lemma OAI.ContingencyTables.CompanionOracleDensity.observed_ratio_bounds line 27
3. lemma OAI.ContingencyTables.CompanionOracleDensity.observed_correction_bounds line 38
4. theorem OAI.ContingencyTables.CompanionOracleDensity.estimateValue_range line 55

   Source documentation

   These bounds hold for every Boolean input, including executions on which the empirical averages are statistically inaccurate.

   theorem estimateValue_range (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 : ℚ) (hd : 0 < delta) (hd1 : delta < 1) (hf : 0 < failure)
       (v : Grid (I := Fin (dimension A)) K) (draws : EstimatorInput A C K j delta failure) :
   …

   Mentions: OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.CompanionOracleDensity.EstimatorInput

5. theorem OAI.ContingencyTables.CompanionOracleDensity.estimateValue_positive line 95