OAI/Combinatorics/ContingencyTables/Dense/DenseAxisSemantics.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Natural coordinate encodings of dense axis moves

  1. lemma OAI.ContingencyTables.DensePrograms.listExchange_increment line 11
  2. lemma OAI.ContingencyTables.DensePrograms.listExchange_decrement line 28
  3. def OAI.ContingencyTables.DensePrograms.gridNatCode line 45
  4. lemma OAI.ContingencyTables.DensePrograms.gridNatCode_getD line 48
  5. lemma OAI.ContingencyTables.DensePrograms.gridNatCode_update line 53
  6. theorem OAI.ContingencyTables.DensePrograms.axisListStep_eq line 66

    Source documentation

    The bounded list operation implements exactly the signed geometric axis proposal, including both boundary rejections.

    theorem axisListStep_eq {q K : ℕ} (a : Grid (I := Fin q) K) (i : Fin q) (sign : Bool) :
…