OAI/Computability/DeterministicSum/Interpolation.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Prime-power Newton interpolation, digit ranks and truncated filters.

  1. def OAI.DeterministicThreeSum.Newton.entry line 15
  2. lemma OAI.DeterministicThreeSum.Newton.entry_zero line 18
  3. lemma OAI.DeterministicThreeSum.Newton.entry_lowerTriangular line 23
  4. lemma OAI.DeterministicThreeSum.Newton.entry_det_unit line 28
  5. def OAI.DeterministicThreeSum.Newton.tensor line 38
  6. lemma OAI.DeterministicThreeSum.Newton.tensor_mul line 42
  7. lemma OAI.DeterministicThreeSum.Newton.tensor_one line 52
  8. def OAI.DeterministicThreeSum.Newton.coefficients line 64
  9. lemma OAI.DeterministicThreeSum.Newton.interpolate line 68
  10. def OAI.DeterministicThreeSum.Newton.degree line 77
  11. lemma OAI.DeterministicThreeSum.Newton.exists_coordinate_lt line 79
  12. lemma OAI.DeterministicThreeSum.Newton.tensor_entry_zero line 85
  13. def OAI.DeterministicThreeSum.Newton.basisPolynomial line 90
  14. lemma OAI.DeterministicThreeSum.Newton.eval_basisPolynomial line 94
  15. def OAI.DeterministicThreeSum.Newton.truncatedPolynomial line 99
  16. theorem OAI.DeterministicThreeSum.Newton.truncated_agreement line 104
  17. lemma OAI.DeterministicThreeSum.Newton.basisPolynomial_degree line 124
  18. lemma OAI.DeterministicThreeSum.Newton.truncatedPolynomial_degree line 148
  19. lemma OAI.DeterministicThreeSum.Newton.coefficients_unique line 158
  20. lemma OAI.DeterministicThreeSum.Newton.small_difference_unit line 166
  21. lemma OAI.DeterministicThreeSum.Newton.primePower_node_units line 181
  22. theorem OAI.DeterministicThreeSum.Newton.primePower_truncated_agreement line 193
  23. def OAI.DeterministicThreeSum.Digits.rank line 209
  24. def OAI.DeterministicThreeSum.Digits.node line 214
  25. lemma OAI.DeterministicThreeSum.Digits.node_rank line 219
  26. lemma OAI.DeterministicThreeSum.Digits.rank_node line 224
  27. lemma OAI.DeterministicThreeSum.Digits.rank_lt line 229
  28. lemma OAI.DeterministicThreeSum.Digits.node_lt line 234
  29. def OAI.DeterministicThreeSum.Digits.order line 239
  30. lemma OAI.DeterministicThreeSum.Digits.order_val line 246
  31. lemma OAI.DeterministicThreeSum.Digits.order_symm_val line 249
  32. def OAI.DeterministicThreeSum.Digits.value line 254
  33. lemma OAI.DeterministicThreeSum.Digits.value_add line 256
  34. lemma OAI.DeterministicThreeSum.Digits.value_succ line 260
  35. lemma OAI.DeterministicThreeSum.Digits.value_lt_pow line 269
  36. lemma OAI.DeterministicThreeSum.Digits.value_injective line 279
  37. def OAI.DeterministicThreeSum.Digits.sumIndex line 300
  38. def OAI.DeterministicThreeSum.Digits.rankTuple line 304
  39. lemma OAI.DeterministicThreeSum.Digits.node_rankTuple line 308
  40. def OAI.DeterministicThreeSum.Digits.cutoff line 313
  41. def OAI.DeterministicThreeSum.Filter.table line 325
  42. def OAI.DeterministicThreeSum.Filter.polynomial line 331
  43. def OAI.DeterministicThreeSum.Filter.exceptionalTuples line 336
  44. def OAI.DeterministicThreeSum.Filter.exceptionalResidues line 340
  45. lemma OAI.DeterministicThreeSum.Filter.exceptionalResidues_subset line 343
  46. lemma OAI.DeterministicThreeSum.Filter.exceptional_card line 349
  47. lemma OAI.DeterministicThreeSum.Filter.rank_sum_le_of_not_exceptional line 353
  48. theorem OAI.DeterministicThreeSum.Filter.agreement line 361
  49. lemma OAI.DeterministicThreeSum.Filter.polynomial_degree line 380