OAI/Combinatorics/ContingencyTables/Machines/BoundedPowerProgram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Reusing a unary allowance across a binary transition table

  1. def OAI.ContingencyTables.BoundedPowerPrograms.powerInput line 10
  2. def OAI.ContingencyTables.BoundedPowerPrograms.powerInputRealizer line 12
  3. lemma OAI.ContingencyTables.BoundedPowerPrograms.polynomial_powerInput line 15
  4. def OAI.ContingencyTables.BoundedPowerPrograms.power line 20
  5. def OAI.ContingencyTables.BoundedPowerPrograms.powerRealizer line 22
  6. theorem OAI.ContingencyTables.BoundedPowerPrograms.polynomial_power line 27

    Source documentation

    A single allowance list can be shared by all entries in the finite matrix. Each binary power then has polynomial cost in the supplied data.

    theorem polynomial_power : PolynomialTime powerRealizer := by
…

    Mentions: OAI.ContingencyTables.BoundedPowerPrograms.powerRealizer

  7. theorem OAI.ContingencyTables.BoundedPowerPrograms.power_eq line 35