OAI/Combinatorics/ContingencyTables/Rooted/RootedComputedEstimator.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The executed blocks have the complete estimator law

Only the physical sample programs differ from the original enumeration. Exact independent-observable transport identifies their whole product estimator, including every event used by the confidence proof.

  1. abbrev OAI.ContingencyTables.RootedComputedEstimator.RatioWords line 25
  2. abbrev OAI.ContingencyTables.RootedComputedEstimator.CorrectionWords line 29
  3. abbrev OAI.ContingencyTables.RootedComputedEstimator.Inputs line 33
  4. def OAI.ContingencyTables.RootedComputedEstimator.ratioAverage line 36
  5. def OAI.ContingencyTables.RootedComputedEstimator.correctionAverage line 43
  6. def OAI.ContingencyTables.RootedComputedEstimator.estimate line 51
  7. lemma OAI.ContingencyTables.RootedComputedEstimator.ratioAverage_law line 58
  8. lemma OAI.ContingencyTables.RootedComputedEstimator.correctionAverage_law line 74
  9. theorem OAI.ContingencyTables.RootedComputedEstimator.sameLaw line 98

    Source documentation

    Exact equality of the whole rational estimator law; no extra oracle or confidence hypothesis is introduced at the implementation boundary.

    theorem sameLaw (A : Instance (Fin m) (Fin n)) (C K j : ℕ)
    (hC : 0 < C) (hj : j ≤ rationalHeight A C) (hK : 1 ≤ K)
    (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=binWidth A C) (delta failure : ℚ)
    (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
    (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K) :
…

    Mentions: OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.RootedCatalogGrid.freeCount