OAI/NumberTheory/Ostmann/Construction/ActualTests.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Construction.residueTest line 10
  2. def OAI.Ostmann.Construction.residueTransform line 14
  3. def OAI.Ostmann.Construction.giantResidueTest line 18
  4. def OAI.Ostmann.Construction.giantResidueTransform line 22
  5. theorem OAI.Ostmann.Construction.residueTest_eq line 25
  6. theorem OAI.Ostmann.Construction.residueTransform_eq line 29
  7. theorem OAI.Ostmann.Construction.giantResidueTest_eq line 33
  8. theorem OAI.Ostmann.Construction.residueTest_fourier line 37
  9. theorem OAI.Ostmann.Construction.giantResidueTest_fourier line 42
  10. theorem OAI.Ostmann.Construction.residueTest_sum_zero line 47
  11. theorem OAI.Ostmann.Construction.giantResidueTransform_norm_le line 51
  12. theorem OAI.Ostmann.Construction.residueTransform_neg line 54
  13. theorem OAI.Ostmann.Construction.giantResidueTransform_neg line 61