OAI/Combinatorics/ContingencyTables/Counting/CompanionMultiplierMatrixProgram.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

The full multiplier update and abort test as list programs

Only the polynomial list of labelled pairs is traversed. Every matrix entry is updated from the actual plain and defect counts of the stored trajectory. The count check includes every off-diagonal labelled type.

  1. abbrev OAI.ContingencyTables.CompanionMultiplierMatrixProgram.FractionMatrix line 20
  2. abbrev OAI.ContingencyTables.CompanionMultiplierMatrixProgram.Input line 21
  3. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.indices line 23
  4. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.indicesRealizer line 25
  5. lemma OAI.ContingencyTables.CompanionMultiplierMatrixProgram.polynomial_indices line 27
  6. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.readEntry line 33
  7. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.readEntryRealizer line 36
  8. lemma OAI.ContingencyTables.CompanionMultiplierMatrixProgram.polynomial_readEntry line 40
  9. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.updateEntry line 46
  10. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.updateEntryRealizer line 49
  11. lemma OAI.ContingencyTables.CompanionMultiplierMatrixProgram.polynomial_updateEntry line 53
  12. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.rowEntry line 60
  13. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.rowEntryRealizer line 63
  14. lemma OAI.ContingencyTables.CompanionMultiplierMatrixProgram.polynomial_rowEntry line 67
  15. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.updateRow line 73
  16. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.updateRowRealizer line 76
  17. lemma OAI.ContingencyTables.CompanionMultiplierMatrixProgram.polynomial_updateRow line 80
  18. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.updateMatrix line 85
  19. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.updateMatrixRealizer line 88
  20. theorem OAI.ContingencyTables.CompanionMultiplierMatrixProgram.polynomial_updateMatrix line 91
  21. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.positiveEntry line 97

    Source documentation

    Diagonal matrix entries do not name defect classes.

    def positiveEntry (z : DefectCountInput) : Bool :=
…
  22. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.positiveEntryRealizer line 100
  23. lemma OAI.ContingencyTables.CompanionMultiplierMatrixProgram.polynomial_positiveEntry line 106
  24. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.positiveRow line 114
  25. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.positiveRowRealizer line 117
  26. lemma OAI.ContingencyTables.CompanionMultiplierMatrixProgram.polynomial_positiveRow line 124
  27. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.positiveCounts line 134
  28. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.positiveCountsRealizer line 137
  29. theorem OAI.ContingencyTables.CompanionMultiplierMatrixProgram.polynomial_positiveCounts line 144
  30. lemma OAI.ContingencyTables.CompanionMultiplierMatrixProgram.positiveCounts_iff line 153
  31. def OAI.ContingencyTables.CompanionMultiplierMatrixProgram.matrixCode line 176
  32. lemma OAI.ContingencyTables.CompanionMultiplierMatrixProgram.readEntry_code line 179
  33. theorem OAI.ContingencyTables.CompanionMultiplierMatrixProgram.updateEntry_code line 184
  34. lemma OAI.ContingencyTables.CompanionMultiplierMatrixProgram.positiveCounts_code line 190
  35. theorem OAI.ContingencyTables.CompanionMultiplierMatrixProgram.updateMatrix_code line 234

    Source documentation

    The executable update contains exactly one entry for every ordered pair of labels, in the same order as the executable proposal catalog.

    theorem updateMatrix_code (states : List (Set (Labels A×Bool)))
    (w : Fin p → Fin p → TreeFraction.Fraction) :
    updateMatrix ((orderedCatalog A g e,states.map (encodeSet e)),matrixCode w)=
      matrixCode (fun i j => updateCode
        (((orderedCatalog A g e,states.map (encodeSet e)),(i.val,j.val)),w i j)) := by
…

    Mentions: OAI.ContingencyTables.CompanionMultiplierMatrixProgram.updateMatrix, OAI.ContingencyTables.CompanionMultiplierMatrixProgram.matrixCode