OAI/Combinatorics/ContingencyTables/Machines/IntegerMatrixProgram.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Binary integer matrix propagation for exact law tabulation

  1. def OAI.ContingencyTables.IntegerMatrixPrograms.dot line 13

    Source documentation

    Missing coordinates are zero. The loop runs over the vector's length.

    def dot (z : List ℕ×List ℕ) : ℕ :=
…
  2. def OAI.ContingencyTables.IntegerMatrixPrograms.entryRealizer line 16
  3. lemma OAI.ContingencyTables.IntegerMatrixPrograms.polynomial_entry line 22
  4. def OAI.ContingencyTables.IntegerMatrixPrograms.dotRealizer line 31
  5. lemma OAI.ContingencyTables.IntegerMatrixPrograms.polynomial_dot line 38
  6. def OAI.ContingencyTables.IntegerMatrixPrograms.propagate line 48

    Source documentation

    A matrix is stored by columns, so each new coordinate is one dot product.

    def propagate (z : List (List ℕ)×List ℕ) : List ℕ :=
…
  7. def OAI.ContingencyTables.IntegerMatrixPrograms.propagateRealizer line 51
  8. lemma OAI.ContingencyTables.IntegerMatrixPrograms.polynomial_propagate line 54
  9. lemma OAI.ContingencyTables.IntegerMatrixPrograms.range_sum line 58
  10. lemma OAI.ContingencyTables.IntegerMatrixPrograms.dot_ofFn line 66
  11. lemma OAI.ContingencyTables.IntegerMatrixPrograms.propagate_ofFn line 74
  12. def OAI.ContingencyTables.IntegerMatrixPrograms.step line 80

    Source documentation

    One iteration retains the transition table unchanged.

    def step (z : ℕ×(List (List ℕ)×List ℕ)) : List (List ℕ)×List ℕ :=
…
  13. def OAI.ContingencyTables.IntegerMatrixPrograms.stepRealizer line 83
  14. lemma OAI.ContingencyTables.IntegerMatrixPrograms.polynomial_step line 86
  15. def OAI.ContingencyTables.IntegerMatrixPrograms.iterate line 90
  16. def OAI.ContingencyTables.IntegerMatrixPrograms.iterateRealizer line 93
  17. lemma OAI.ContingencyTables.IntegerMatrixPrograms.countDown_table line 96
  18. lemma OAI.ContingencyTables.IntegerMatrixPrograms.iterate_succ line 102
  19. lemma OAI.ContingencyTables.IntegerMatrixPrograms.iterate_ofFn line 105
  20. lemma OAI.ContingencyTables.IntegerMatrixPrograms.dot_nil line 129
  21. lemma OAI.ContingencyTables.IntegerMatrixPrograms.dot_cons line 131
  22. lemma OAI.ContingencyTables.IntegerMatrixPrograms.dot_le line 142
  23. def OAI.ContingencyTables.IntegerMatrixPrograms.matrixTotal line 154
  24. lemma OAI.ContingencyTables.IntegerMatrixPrograms.propagate_sum_le line 156
  25. lemma OAI.ContingencyTables.IntegerMatrixPrograms.sum_size_le_weight line 165
  26. lemma OAI.ContingencyTables.IntegerMatrixPrograms.matrixTotal_size_le_weight line 175
  27. lemma OAI.ContingencyTables.IntegerMatrixPrograms.pow_size_le line 187
  28. lemma OAI.ContingencyTables.IntegerMatrixPrograms.weight_of_entry_bound line 195
  29. theorem OAI.ContingencyTables.IntegerMatrixPrograms.work_iterate line 206

    Source documentation

    The iteration bound uses the number of steps and the binary input size. The numerical values of the matrix entries never control a loop.

    theorem work_iterate : WorkBound iterateRealizer
    (fun z => z.1+weight z.2) := by
…

    Mentions: OAI.ContingencyTables.IntegerMatrixPrograms.iterateRealizer