OAI/Combinatorics/ContingencyTables/Counting/CompanionOracleEstimator.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionOracleDensity.rationalAverage line 19
2. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalAverage_cast line 22
3. abbrev OAI.ContingencyTables.CompanionOracleDensity.RatioBlock line 26
4. abbrev OAI.ContingencyTables.CompanionOracleDensity.CorrectionBlock line 29
5. abbrev OAI.ContingencyTables.CompanionOracleDensity.EstimatorInput line 33
6. def OAI.ContingencyTables.CompanionOracleDensity.observedFactor line 36
7. def OAI.ContingencyTables.CompanionOracleDensity.targetFactor line 48
8. def OAI.ContingencyTables.CompanionOracleDensity.estimateValue line 53
9. theorem OAI.ContingencyTables.CompanionOracleDensity.targetFactor_product line 60

   Source documentation

   The exact means appearing in the implemented product telescope to h, including the integer-population correction and the free-assignment count.

   theorem targetFactor_product (A : Instance I J) (C : ℕ) (hC : 0 < C) (z : View A → ℕ)
       (K : ℕ) (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (j : ℕ) :
       (assignmentCount A:ℝ)*(∏ i,targetFactor A C z K hK hW j i)=
         h A ((j:ℝ)*C/height A C) z := by
   …

   Mentions: OAI.ContingencyTables.CompanionOracleDensity.assignmentCount, OAI.ContingencyTables.CompanionOracleDensity.targetFactor, OAI.ContingencyTables.CompanionOracleDensity.height

10. lemma OAI.ContingencyTables.CompanionOracleDensity.targetFactor_positive line 73
11. def OAI.ContingencyTables.CompanionOracleDensity.GoodEstimate line 87
12. def OAI.ContingencyTables.CompanionOracleDensity.innerTolerance line 93
13. theorem OAI.ContingencyTables.CompanionOracleDensity.goodEstimate_accuracy line 97

    Source documentation

    On the event certified by the actual independent block experiments, the returned rational product estimates the literal original h-value.

    theorem goodEstimate_accuracy (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)
        (v : Grid (I := Fin (dimension A)) K)
    …

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