OAI/Combinatorics/ContingencyTables/Rooted/RootedEstimatorAmplification.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic confidence amplification of the actual weight estimator

  1. def OAI.ContingencyTables.RootedOracleDensity.medianEstimate line 20
  2. theorem OAI.ContingencyTables.RootedOracleDensity.medianEstimate_success line 29
  3. theorem OAI.ContingencyTables.RootedOracleDensity.medianEstimate_range line 81

    Source documentation

    Amplification also preserves the proved range on every word, including statistically unsuccessful words.

    theorem medianEstimate_range (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 delta : ℚ) (he0 : 0 < epsilon) (he1 : epsilon < 1)
    (v : Grid (I := Fin (dimension A)) K)
…

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