OAI/Combinatorics/ContingencyTables/Counting/CountingPhaseSchedule.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Explicit scalar schedules for the adaptive counting phases

Every precision and sample length below is a rational or natural arithmetic expression. In particular the dyadic exponents use a polynomial reciprocal allowance, so no real logarithm is evaluated by the algorithm.

  1. def OAI.ContingencyTables.CountingPhaseSchedule.tolerance line 17

    Source documentation

    Per-phase logarithmic tolerance.

    def tolerance (H : ℕ) (epsilon : ℚ) : ℚ := epsilon/(800*(H+1))
  2. def OAI.ContingencyTables.CountingPhaseSchedule.observable line 20

    Source documentation

    The integer form of the manuscript's observable coefficient.

    def observable (p W : ℕ) : ℕ :=
…
  3. def OAI.ContingencyTables.CountingPhaseSchedule.observationCoefficient line 23
  4. def OAI.ContingencyTables.CountingPhaseSchedule.observations line 25
  5. def OAI.ContingencyTables.CountingPhaseSchedule.returnCap line 28
  6. def OAI.ContingencyTables.CountingPhaseSchedule.noiseCoefficient line 30
  7. def OAI.ContingencyTables.CountingPhaseSchedule.precision line 32
  8. def OAI.ContingencyTables.CountingPhaseSchedule.noise line 35
  9. def OAI.ContingencyTables.CountingPhaseSchedule.initialPrecision line 38
  10. lemma OAI.ContingencyTables.CountingPhaseSchedule.tolerance_pos line 40
  11. lemma OAI.ContingencyTables.CountingPhaseSchedule.tolerance_le_quarter line 45
  12. lemma OAI.ContingencyTables.CountingPhaseSchedule.observations_pos line 52
  13. lemma OAI.ContingencyTables.CountingPhaseSchedule.returnCap_pos line 56
  14. lemma OAI.ContingencyTables.CountingPhaseSchedule.precision_pos line 60
  15. lemma OAI.ContingencyTables.CountingPhaseSchedule.noise_pos line 64
  16. lemma OAI.ContingencyTables.CountingPhaseSchedule.noise_le_tolerance line 68
  17. lemma OAI.ContingencyTables.CountingPhaseSchedule.reciprocal_two_pow line 81
  18. lemma OAI.ContingencyTables.CountingPhaseSchedule.precision_error line 86
  19. lemma OAI.ContingencyTables.CountingPhaseSchedule.initial_error line 91
  20. lemma OAI.ContingencyTables.CountingPhaseSchedule.observations_error line 105
  21. lemma OAI.ContingencyTables.CountingPhaseSchedule.cap_error line 124
  22. lemma OAI.ContingencyTables.CountingPhaseSchedule.noise_error line 141
  23. lemma OAI.ContingencyTables.CountingPhaseSchedule.logarithmic_error line 156
  24. lemma OAI.ContingencyTables.CountingPhaseSchedule.combine_error line 175

    Source documentation

    The four error terms correspond to empirical observations, initialization, restart caps and the accumulated query/transition error.

    lemma combine_error (p H tau N n k h : ℕ) (c eta xi allowance : ℝ)
    (hxi : 0 ≤ xi) (hprec : 1/(2:ℝ)^k ≤ xi)
    (hobs : c/(((N+1:ℕ):ℝ)*eta^2) ≤ allowance)
    (hinit : 2/(2:ℝ)^h ≤ allowance)
    (hcap : 40*(H:ℝ)*tau*p^2/(n:ℝ) ≤ allowance)
    (hnoise : (noiseCoefficient H tau N n:ℝ)*xi ≤ allowance) :
    c/(((N+1:ℕ):ℝ)*eta^2)+
      (N:ℝ)*((6*xi+1/(2:ℝ)^k)/2)+
      2*(1/(2:ℝ)^h+(H:ℝ)*((tau:ℝ)*
        (20*(p:ℝ)^2/n+((n+1:ℕ):ℝ)*((6*xi+1/(2:ℝ)^k)/2))))+
      2*((N+1:ℕ):ℝ)*xi ≤ 4*allowance := by
…

    Mentions: OAI.ContingencyTables.CountingPhaseSchedule.noiseCoefficient