OAI/Combinatorics/ContingencyTables/Machines/FixedCardinalityProgram.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial binary arithmetic for sequential subset inclusion

The rational inclusion threshold is computed by an integer product and quotient. In particular the denominator is never expanded into a unary loop; the only exponential integer has the supplied word length as its binary length.

  1. abbrev OAI.ContingencyTables.FixedCardinalityProgram.HeadInput line 18
  2. def OAI.ContingencyTables.FixedCardinalityProgram.includeCode line 20
  3. def OAI.ContingencyTables.FixedCardinalityProgram.includeRealizer line 23
  4. theorem OAI.ContingencyTables.FixedCardinalityProgram.polynomial_include line 34
  5. theorem OAI.ContingencyTables.FixedCardinalityProgram.inclusion_threshold line 50
  6. theorem OAI.ContingencyTables.FixedCardinalityProgram.includeCode_ofFn line 68

    Source documentation

    The executable natural-number comparison is exactly the inclusion decision in the finite Boolean law.

    theorem includeCode_ofFn (B n k : ℕ) (bits : Fin B → Bool) :
    includeCode ((n+1,k),List.ofFn bits)=FixedCardinalityBits.headDraw B n k bits := by
…

    Mentions: OAI.ContingencyTables.FixedCardinalityProgram.includeCode, OAI.ContingencyTables.FixedCardinalityBits.headDraw