OAI/Combinatorics/ContingencyTables/Counting/CountingScheduleSizes.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Polynomial numeric bounds for the explicit counting schedules

  1. lemma OAI.ContingencyTables.CountingPhaseSchedule.inverse_tolerance_le line 11

    Source documentation

    A natural reciprocal-accuracy allowance bounds the rational inverse tolerance; no logarithmic operation is used.

    lemma inverse_tolerance_le (H E : ℕ) (epsilon : ℚ) (he : 0 < epsilon)
    (hE : 1/epsilon ≤ (E:ℚ)) :
    1/tolerance H epsilon ≤ (800*(H+1)*E:ℕ) := by
…

    Mentions: OAI.ContingencyTables.CountingPhaseSchedule.tolerance

  2. def OAI.ContingencyTables.CountingPhaseSchedule.observationBound line 21
  3. lemma OAI.ContingencyTables.CountingPhaseSchedule.observations_le line 24
  4. def OAI.ContingencyTables.CountingPhaseSchedule.precisionBound line 43
  5. lemma OAI.ContingencyTables.CountingPhaseSchedule.precision_le line 47
  6. lemma OAI.ContingencyTables.CountingPhaseSchedule.returnCap_eq line 63
  7. lemma OAI.ContingencyTables.CountingPhaseSchedule.initialPrecision_eq line 66