OAI/Computability/DeterministicSum/PaddedMaps.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Charged padded matrix maps and interleaved coordinate layouts.

  1. abbrev OAI.DeterministicThreeSum.Structured.Indexed.PaddedAxis.inputSize line 13
  2. def OAI.DeterministicThreeSum.Structured.Indexed.PaddedAxis.limitAddress line 14
  3. def OAI.DeterministicThreeSum.Structured.Indexed.PaddedAxis.term line 16
  4. def OAI.DeterministicThreeSum.Structured.Indexed.PaddedAxis.row line 18
  5. def OAI.DeterministicThreeSum.Structured.Indexed.PaddedAxis.pass line 19
  6. def OAI.DeterministicThreeSum.Structured.Indexed.PaddedAxis.pad line 20
  7. lemma OAI.DeterministicThreeSum.Structured.Indexed.PaddedAxis.addresses_valid line 22
  8. lemma OAI.DeterministicThreeSum.Structured.Indexed.PaddedAxis.limitAddress_value line 55
  9. lemma OAI.DeterministicThreeSum.Structured.Indexed.PaddedAxis.row_valid line 59
  10. lemma OAI.DeterministicThreeSum.Structured.Indexed.PaddedAxis.row_value line 79
  11. lemma OAI.DeterministicThreeSum.Structured.Indexed.PaddedAxis.row_reads_outside line 94
  12. theorem OAI.DeterministicThreeSum.Structured.Indexed.PaddedAxis.pass_correct line 113
  13. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.pairCode line 168
  14. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.digit_lt line 172
  15. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.pairCode_lt line 176
  16. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.packed_div line 187
  17. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.packed_mod line 189
  18. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.packed_lt line 192
  19. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.pairCode_injective line 201
  20. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.pairIndex line 221
  21. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.tripleIndex line 229
  22. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.tripleIndex_val line 232
  23. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.sourceIndex_packed line 236
  24. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.coefficientIndex_packed line 241
  25. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.padded_left_read line 252
  26. theorem OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.left_level_value line 280
  27. theorem OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.right_level_value line 307
  28. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.parent_packed line 320
  29. theorem OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.combine_level_value line 334
  30. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.input_padding_bound line 362
  31. theorem OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.left_level_correct line 369