OAI/Combinatorics/ContingencyTables/Rooted/RootedOracleEstimator.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.RootedOracleDensity.observedFactor line 21
2. def OAI.ContingencyTables.RootedOracleDensity.targetFactor line 33
3. def OAI.ContingencyTables.RootedOracleDensity.estimateValue line 38
4. theorem OAI.ContingencyTables.RootedOracleDensity.targetFactor_product line 45

   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) (R : RootedCompletion.Selection A.T) (C : ℕ) (hC : 0 < C) (z : View A → ℕ)
       (K : ℕ) (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (j : ℕ) :
       (assignmentCount A:ℝ)*(∏ i,targetFactor A R C z K hK hW j i)=
         RootedCountIdentification.h A R ((j:ℝ)*C/height A C) z := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedOracleDensity.targetFactor, OAI.ContingencyTables.RootedCountIdentification.h

5. lemma OAI.ContingencyTables.RootedOracleDensity.targetFactor_positive line 58
6. def OAI.ContingencyTables.RootedOracleDensity.GoodEstimate line 72
7. theorem OAI.ContingencyTables.RootedOracleDensity.goodEstimate_accuracy line 80

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

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.BalancedBox.InBox