OAI/Computability/DeterministicSum/NewtonCoefficients.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Exact transform coefficients and integer-table compilation.

  1. def OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.digitFunction line 15
  2. def OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.functionDigit line 19
  3. lemma OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.functionDigit_digitFunction line 23
  4. lemma OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.digitFunction_functionDigit line 29
  5. def OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.digitFunctionEquiv line 35
  6. lemma OAI.DeterministicThreeSum.Structured.Indexed.SparseAxis.digitCoefficient_product line 41
  7. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.value_cons line 56
  8. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.digitCode_degree line 71
  9. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.inverseTable line 79
  10. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.conversionTable line 84
  11. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.inverseTable_entry line 89
  12. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.conversionTable_entry line 99
  13. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.tensorValue_coefficients line 109
  14. theorem OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.output_source line 122
  15. def OAI.DeterministicThreeSum.Structured.Indexed.integerCommand line 154
  16. def OAI.DeterministicThreeSum.Structured.Indexed.integerValue line 162
  17. lemma OAI.DeterministicThreeSum.Structured.Indexed.integerValue_lt line 165
  18. lemma OAI.DeterministicThreeSum.Structured.Indexed.integerValue_cast line 168
  19. lemma OAI.DeterministicThreeSum.Structured.Indexed.integerCommand_correct line 179
  20. def OAI.DeterministicThreeSum.Structured.Indexed.integerTable line 200
  21. def OAI.DeterministicThreeSum.Structured.Indexed.integerTableMemory line 206
  22. lemma OAI.DeterministicThreeSum.Structured.Indexed.integerTable_correct line 210