OAI/Combinatorics/ContingencyTables/Machines/BinaryPowerProgram.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Binary powers with a polynomial bound in the exponent and input bits

  1. def OAI.ContingencyTables.BinaryPowerPrograms.setup line 11
  2. def OAI.ContingencyTables.BinaryPowerPrograms.singleton line 13
  3. lemma OAI.ContingencyTables.BinaryPowerPrograms.polynomial_singleton line 16
  4. def OAI.ContingencyTables.BinaryPowerPrograms.setupRealizer line 20
  5. lemma OAI.ContingencyTables.BinaryPowerPrograms.polynomial_setup line 23
  6. def OAI.ContingencyTables.BinaryPowerPrograms.power line 28
  7. def OAI.ContingencyTables.BinaryPowerPrograms.powerRealizer line 30
  8. theorem OAI.ContingencyTables.BinaryPowerPrograms.power_eq line 33
  9. theorem OAI.ContingencyTables.BinaryPowerPrograms.work_power line 49

    Source documentation

    Multiplication uses binary operands; only the exponent controls the number of iterations. This is sufficient for the dyadic tabulation.

    theorem work_power : WorkBound powerRealizer (fun z => z.2+weight z.1) := by
…

    Mentions: OAI.ContingencyTables.BinaryPowerPrograms.powerRealizer