OAI/Computability/DeterministicSum/NewtonTables.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Prime-power coefficient tables and their paid Newton transforms.

  1. lemma OAI.DeterministicThreeSum.Newton.entry_map line 14
  2. lemma OAI.DeterministicThreeSum.Newton.cast_natAbs_unit line 19
  3. def OAI.DeterministicThreeSum.Newton.inverseDenominator line 27
  4. def OAI.DeterministicThreeSum.Newton.inverseNumerator line 30
  5. lemma OAI.DeterministicThreeSum.Newton.inverseDenominator_unit line 34
  6. lemma OAI.DeterministicThreeSum.Newton.inverseDenominator_prime line 46
  7. lemma OAI.DeterministicThreeSum.Newton.inverseInteger_eq line 51
  8. lemma OAI.DeterministicThreeSum.Newton.inverse_entry_integer line 62
  9. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonTable.numeratorAt line 76
  10. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonTable.numerators line 83
  11. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonTable.command line 86
  12. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonTable.numeratorAt_entry line 89
  13. theorem OAI.DeterministicThreeSum.Structured.Indexed.NewtonTable.command_correct line 100
  14. lemma OAI.DeterministicThreeSum.Newton.univariate_integer line 139
  15. lemma OAI.DeterministicThreeSum.Newton.conversion_integer line 143
  16. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonConversionTable.integerAt line 154
  17. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonConversionTable.integers line 161
  18. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonConversionTable.command line 164
  19. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonConversionTable.integerAt_entry line 167
  20. theorem OAI.DeterministicThreeSum.Structured.Indexed.NewtonConversionTable.command_correct line 178
  21. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.inverseTable_lt line 209
  22. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.conversionTable_lt line 215
  23. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.memory_inverse line 221
  24. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.memory_conversion line 240
  25. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.tableSources line 259
  26. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.tableValues line 262
  27. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.tableSetup_correct line 265
  28. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.initialSources line 276
  29. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.initialSetup_correct line 280
  30. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.paidCommand line 296
  31. theorem OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.paidCommand_correct line 306