OAI/Combinatorics/ContingencyTables/Dense/DenseAxisWordProgram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Binary-word decoding for a dense coordinate proposal

  1. abbrev OAI.ContingencyTables.DensePrograms.AxisWordData line 11
  2. def OAI.ContingencyTables.DensePrograms.axisWordStep line 13
  3. def OAI.ContingencyTables.DensePrograms.axisWordStepRealizer line 16
  4. theorem OAI.ContingencyTables.DensePrograms.polynomial_axisWordStep line 22
  5. lemma OAI.ContingencyTables.DensePrograms.directionCode_first line 34
  6. lemma OAI.ContingencyTables.DensePrograms.directionCode_second line 37
  7. theorem OAI.ContingencyTables.DensePrograms.axisWordStep_eq line 45

    Source documentation

    A binary index gives exactly the signed coordinate code used by the finite dense-chain transition; unused indices still reject.

    theorem axisWordStep_eq {q K k : ℕ} (a : Grid (I := Fin q) K) (bits : Fin k → Bool) :
…