OAI/Geometry/PeriodicTiling/FiniteDifferencePolynomial.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PeriodicTilingThree.intSequence_eq_of_forwardDiff_eq line 21
  2. def OAI.PeriodicTilingThree.newtonSequence line 40
  3. theorem OAI.PeriodicTilingThree.newtonSequence_cons line 43
  4. theorem OAI.PeriodicTilingThree.newtonSequence_cons_zero line 50
  5. theorem OAI.PeriodicTilingThree.forwardDiff_newtonSequence_cons line 54
  6. theorem OAI.PeriodicTilingThree.exists_newtonSequence_of_iter_forwardDiff_eq_zero line 72
  7. def OAI.PeriodicTilingThree.newtonBasisPolynomial line 93
  8. theorem OAI.PeriodicTilingThree.descPochhammer_eval_int_eq_factorial_mul_choose line 96
  9. theorem OAI.PeriodicTilingThree.newtonBasisPolynomial_eval_int line 104
  10. def OAI.PeriodicTilingThree.newtonPolynomial line 110
  11. theorem OAI.PeriodicTilingThree.newtonPolynomial_eval_int line 113
  12. theorem OAI.PeriodicTilingThree.exists_polynomial_lift_of_iter_forwardDiff_eq_zero line 123