OAI/Computability/DeterministicSum/SparseCodes.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Sparse digit coding and low-degree transform identification.

  1. def OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.lowCode line 11
  2. lemma OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.lowCode_lt line 15
  3. lemma OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.lowCode_sum line 30
  4. lemma OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.digitCode_sum line 41
  5. def OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.reverseDigit line 54
  6. lemma OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.digitFunction_reverse line 56
  7. lemma OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.reverseDigit_twice line 59
  8. def OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.reverseEquiv line 65
  9. lemma OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.digitCode_reverse line 67
  10. lemma OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.lowCode_reverse line 79
  11. lemma OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.digitCoefficient_reverse line 82
  12. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.tensorValue_low line 95
  13. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.lowCode_degree line 107
  14. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.tensorValue_coefficients_low line 112
  15. theorem OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.output_source_low line 125
  16. theorem OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.paidCommand_source_low line 158