OAI/NumberTheory/Ostmann/Construction/ConstructedHistoryGuards.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact range and residue guards for the reconstructed original pivots

  1. def OAI.Ostmann.formulaPolynomial line 12
  2. theorem OAI.Ostmann.formulaPolynomial_degree line 16
  3. def OAI.Ostmann.formulaRangePolynomials line 20
  4. theorem OAI.Ostmann.formulaRangePolynomials_iff line 26
  5. theorem OAI.Ostmann.formulaRangePolynomials_degree line 34
  6. theorem OAI.Ostmann.formulaPolynomial_integer_value line 54
  7. theorem OAI.Ostmann.reconstructedPivot_ranges line 68
  8. def OAI.Ostmann.reconstructedHistoryAmplitude line 82
  9. theorem OAI.Ostmann.reconstructedHistoryAmplitude_exact line 90