OAI/Combinatorics/ContingencyTables/Rooted/RootedCountingAmplification.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic confidence for the actual adaptive counting estimator

  1. def OAI.ContingencyTables.RootedCountingAmplification.bitCount line 20
  2. def OAI.ContingencyTables.RootedCountingAmplification.estimate line 23
  3. theorem OAI.ContingencyTables.RootedCountingAmplification.success line 31

    Source documentation

    The confidence parameter changes only the number of independent complete runs, never the internal per-oracle failure allowance.

    theorem success (A : Instance I J) (R : RootedCompletion.Selection A.T)
    (C K H L : ℕ) (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W)
    (epsilon delta : ℚ) (he0 : 0 < epsilon) (he1 : epsilon < 1) (hd : 0 < delta)
    (v : Grid (I := Fin (dimension A)) K) (E : Endpoints A)
…

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection

  4. lemma OAI.ContingencyTables.RootedCountingAmplification.bitCount_eq line 96