OAI/Combinatorics/ContingencyTables/Dense/DenseAxisProgram.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded binary coordinate moves in the dense grid

  1. abbrev OAI.ContingencyTables.DensePrograms.AxisData line 12
  2. def OAI.ContingencyTables.DensePrograms.axisListStep line 14
  3. def OAI.ContingencyTables.DensePrograms.axisListStepRealizer line 25
  4. theorem OAI.ContingencyTables.DensePrograms.polynomial_axisListStep line 45

    Source documentation

    An invalid or boundary move terminates immediately. Its index is never used as an iteration count.

    theorem polynomial_axisListStep : PolynomialTime axisListStepRealizer := by
…

    Mentions: OAI.ContingencyTables.DensePrograms.axisListStepRealizer