OAI/Combinatorics/ContingencyTables/Sampling/ProfileMatrixEntry.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Executable entries of the finite profile transition matrix

  1. abbrev OAI.ContingencyTables.ProfilePrograms.MatrixParameters line 11
  2. abbrev OAI.ContingencyTables.ProfilePrograms.MatrixEntryInput line 12
  3. def OAI.ContingencyTables.ProfilePrograms.matrixData line 14
  4. def OAI.ContingencyTables.ProfilePrograms.matrixDataRealizer line 16
  5. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_matrixData line 19
  6. def OAI.ContingencyTables.ProfilePrograms.sourceData line 23
  7. def OAI.ContingencyTables.ProfilePrograms.sourceDataRealizer line 26
  8. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_sourceData line 30
  9. def OAI.ContingencyTables.ProfilePrograms.targetData line 35
  10. def OAI.ContingencyTables.ProfilePrograms.targetDataRealizer line 38
  11. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_targetData line 42
  12. def OAI.ContingencyTables.ProfilePrograms.entryCacheParameters line 47
  13. def OAI.ContingencyTables.ProfilePrograms.entryCacheParametersRealizer line 50
  14. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_entryCacheParameters line 57
  15. def OAI.ContingencyTables.ProfilePrograms.entryQuery line 67
  16. def OAI.ContingencyTables.ProfilePrograms.entryQueryRealizer line 70
  17. def OAI.ContingencyTables.ProfilePrograms.validMatrixEntry line 76
  18. def OAI.ContingencyTables.ProfilePrograms.validMatrixEntryRealizer line 78
  19. def OAI.ContingencyTables.ProfilePrograms.matrixDenominator line 82

    Source documentation

    The denominator includes the proposal word and its padded completion word.

    def matrixDenominator (z : MatrixParameters) : ℕ :=
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.MatrixParameters

  20. def OAI.ContingencyTables.ProfilePrograms.matrixDenominatorRealizer line 85
  21. def OAI.ContingencyTables.ProfilePrograms.diagonalMatrixEntry line 89
  22. def OAI.ContingencyTables.ProfilePrograms.diagonalMatrixEntryRealizer line 92
  23. def OAI.ContingencyTables.ProfilePrograms.matrixEntry line 101

    Source documentation

    Invalid source vectors are stationary. Invalid target vectors have zero weight from every valid source.

    def matrixEntry (z : MatrixEntryInput) : ℕ :=
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.MatrixEntryInput

  24. def OAI.ContingencyTables.ProfilePrograms.matrixEntryRealizer line 106