OAI/Combinatorics/ContingencyTables/Counting/CountingTerminalSchedule.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Executing the terminal coefficient without real logarithms

The source's ceiling of log₂(1/epsilon) is exactly the natural ceiling logarithm of ceil(1/epsilon). All terminal metadata can therefore be computed with natural and rational arithmetic.

  1. lemma OAI.ContingencyTables.CountingTerminalSchedule.natCeil_ratCast line 20
  2. def OAI.ContingencyTables.CountingTerminalSchedule.precision line 27
  3. def OAI.ContingencyTables.CountingTerminalSchedule.allowance line 28
  4. def OAI.ContingencyTables.CountingTerminalSchedule.coefficient line 29
  5. lemma OAI.ContingencyTables.CountingTerminalSchedule.precision_eq line 32
  6. lemma OAI.ContingencyTables.CountingTerminalSchedule.allowance_eq line 43
  7. lemma OAI.ContingencyTables.CountingTerminalSchedule.coefficient_eq line 47
  8. def OAI.ContingencyTables.CountingTerminalSchedule.capacityBits line 68

    Source documentation

    The full product allowance is computed from the input capacities' binary lengths, rather than supplied as a counting hypothesis.

    def capacityBits (A : Instance I J) : ℕ :=
…
  9. lemma OAI.ContingencyTables.CountingTerminalSchedule.capacity_product_bound line 71
  10. lemma OAI.ContingencyTables.CountingTerminalSchedule.small_product_bound line 78
  11. lemma OAI.ContingencyTables.CountingTerminalSchedule.finalPhase_eq line 93
  12. lemma OAI.ContingencyTables.CountingTerminalSchedule.coefficient_pos line 99