OAI/NumberTheory/Ostmann/Construction/HistoryCoefficientData.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The finite data of one fully substituted history coefficient

  1. structure OAI.Ostmann.HistoryCoefficientData line 11
  2. def OAI.Ostmann.HistoryCoefficientData.value line 32
  3. def OAI.Ostmann.HistoryCoefficientData.factors line 36
  4. def OAI.Ostmann.HistoryCoefficientData.polynomials line 41
  5. def OAI.Ostmann.HistoryCoefficientData.keep line 46
  6. def OAI.Ostmann.HistoryCoefficientData.budget line 50
  7. def OAI.Ostmann.HistoryCoefficientData.complexity line 53
  8. theorem OAI.Ostmann.HistoryCoefficientData.budget_nonneg line 56
  9. theorem OAI.Ostmann.HistoryCoefficientData.factors_budget line 59
  10. theorem OAI.Ostmann.HistoryCoefficientData.polynomials_complexity line 62
  11. theorem OAI.Ostmann.HistoryCoefficientData.value_local line 67