OAI/Combinatorics/ContingencyTables/Machines/TranslationDecisionProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Binary arithmetic for the completion translation test

  1. abbrev OAI.ContingencyTables.DensePrograms.MarginPair line 14
  2. abbrev OAI.ContingencyTables.DensePrograms.TranslationCell line 15
  3. abbrev OAI.ContingencyTables.DensePrograms.TranslationData line 16
  4. def OAI.ContingencyTables.DensePrograms.starParts line 18
  5. def OAI.ContingencyTables.DensePrograms.starPartsRealizer line 21
  6. theorem OAI.ContingencyTables.DensePrograms.polynomial_starParts line 24
  7. def OAI.ContingencyTables.DensePrograms.translationParts line 29
  8. def OAI.ContingencyTables.DensePrograms.translationPartsRealizer line 34
  9. theorem OAI.ContingencyTables.DensePrograms.polynomial_translationParts line 44
  10. def OAI.ContingencyTables.DensePrograms.translatedCell line 60
  11. def OAI.ContingencyTables.DensePrograms.translatedCellRealizer line 64
  12. theorem OAI.ContingencyTables.DensePrograms.polynomial_translatedCell line 72
  13. def OAI.ContingencyTables.DensePrograms.translationValid line 88
  14. def OAI.ContingencyTables.DensePrograms.translationValidRealizer line 91
  15. theorem OAI.ContingencyTables.DensePrograms.polynomial_translationValid line 96
  16. lemma OAI.ContingencyTables.DensePrograms.starParts_code line 101
  17. lemma OAI.ContingencyTables.DensePrograms.translationParts_code line 110
  18. lemma OAI.ContingencyTables.DensePrograms.tableOutput_entry line 126
  19. theorem OAI.ContingencyTables.DensePrograms.translatedCell_code line 142

    Source documentation

    Each binary comparison is the literal translated nonnegativity condition in the Markov-chain acceptance decision.

    theorem translatedCell_code {m n : ℕ}
    (R₀ R₁ : Option (Fin m) → ℕ) (P₀ P₁ : Option (Fin n) → ℕ)
    (X : Table R₀ P₀) (i : Option (Fin m)) (j : Option (Fin n)) :
    translatedCell ((((marginCode R₀,marginCode P₀),(marginCode R₁,marginCode P₁)),
      tableOutput X),(optionIndex i,optionIndex j))=true ↔
      0 ≤ (X.val i j:ℤ)+between R₀ R₁ P₀ P₁ i j := by
…

    Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.DensePrograms.translatedCell, OAI.ContingencyTables.DensePrograms.marginCode, OAI.ContingencyTables.DensePrograms.tableOutput, OAI.ContingencyTables.DensePrograms.optionIndex