OAI/Combinatorics/ContingencyTables/Dense/DenseScaleMatrixProgram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Scaling a binary grid matrix to its integer bin corner

  1. def OAI.ContingencyTables.DensePrograms.scaleRows line 10
  2. def OAI.ContingencyTables.DensePrograms.scaleColumns line 11
  3. def OAI.ContingencyTables.DensePrograms.scaleRowsRealizer line 13
  4. def OAI.ContingencyTables.DensePrograms.scaleColumnsRealizer line 17
  5. lemma OAI.ContingencyTables.DensePrograms.polynomial_scaleRows line 21
  6. lemma OAI.ContingencyTables.DensePrograms.polynomial_scaleColumns line 33
  7. def OAI.ContingencyTables.DensePrograms.scaleRowEntry line 45
  8. def OAI.ContingencyTables.DensePrograms.scaleRowEntryRealizer line 48
  9. lemma OAI.ContingencyTables.DensePrograms.polynomial_scaleRowEntry line 52
  10. def OAI.ContingencyTables.DensePrograms.scaleRow line 58
  11. def OAI.ContingencyTables.DensePrograms.scaleRowRealizer line 61
  12. lemma OAI.ContingencyTables.DensePrograms.polynomial_scaleRow line 64
  13. def OAI.ContingencyTables.DensePrograms.scaleMatrix line 69
  14. def OAI.ContingencyTables.DensePrograms.scaleMatrixRealizer line 72
  15. theorem OAI.ContingencyTables.DensePrograms.polynomial_scaleMatrix line 75
  16. lemma OAI.ContingencyTables.DensePrograms.scaleRow_code line 81
  17. theorem OAI.ContingencyTables.DensePrograms.scaleMatrix_code line 98

    Source documentation

    Every free entry is the integer width times the selected grid corner.

    theorem scaleMatrix_code (R : Option (Fin m) → ℕ) (P : Option (Fin n) → ℕ)
    (d : ℕ) (a : Grid (I := Fin q) K) (e : Fin m×Fin n ≃ Fin q) :
…