OAI/NumberTheory/Ostmann/Preliminaries/FinitePolynomialTail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Rectangular polynomial truncation with a geometric error

  1. theorem OAI.Ostmann.finite_geometric_tail_le line 11
  2. theorem OAI.Ostmann.finite_geometric_sum_le line 21
  3. def OAI.Ostmann.rectangularPolynomialSum line 26
  4. theorem OAI.Ostmann.rectangularPolynomialSum_error line 31