OAI/NumberTheory/Ostmann/SchwartzCutoff.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.SchwartzCutoff.bump line 10
  2. lemma OAI.Ostmann.SchwartzCutoff.bump_zero line 13
  3. lemma OAI.Ostmann.SchwartzCutoff.bump_complex_compact line 16
  4. def OAI.Ostmann.SchwartzCutoff.bumpSchwartz line 19
  5. lemma OAI.Ostmann.SchwartzCutoff.bumpSchwartz_apply line 22
  6. lemma OAI.Ostmann.SchwartzCutoff.fourier_real_conj line 24
  7. lemma OAI.Ostmann.SchwartzCutoff.bump_fourier_even line 35
  8. lemma OAI.Ostmann.SchwartzCutoff.bump_fourier_im line 42
  9. lemma OAI.Ostmann.SchwartzCutoff.bump_fourier_re line 46
  10. lemma OAI.Ostmann.SchwartzCutoff.bump_fourier_re_pos line 66
  11. theorem OAI.Ostmann.SchwartzCutoff.bump_fourier_uniform_lower line 93
  12. lemma OAI.Ostmann.SchwartzCutoff.bumpSchwartz_zero_of_abs_ge line 102
  13. def OAI.Ostmann.SchwartzCutoff.convolutionBump line 107
  14. def OAI.Ostmann.SchwartzCutoff.psi line 110
  15. lemma OAI.Ostmann.SchwartzCutoff.psi_apply line 112
  16. lemma OAI.Ostmann.SchwartzCutoff.psi_im line 115
  17. lemma OAI.Ostmann.SchwartzCutoff.psi_re line 118
  18. lemma OAI.Ostmann.SchwartzCutoff.psi_nonneg line 121
  19. lemma OAI.Ostmann.SchwartzCutoff.psi_even line 125
  20. lemma OAI.Ostmann.SchwartzCutoff.psi_pos line 128
  21. theorem OAI.Ostmann.SchwartzCutoff.psi_uniform_lower line 132
  22. lemma OAI.Ostmann.SchwartzCutoff.convolutionBump_zero_of_abs_ge line 139
  23. lemma OAI.Ostmann.SchwartzCutoff.fourier_twice line 156
  24. theorem OAI.Ostmann.SchwartzCutoff.fourier_psi_zero_of_abs_ge line 162
  25. lemma OAI.Ostmann.SchwartzCutoff.hasCompactSupport_fourier_psi line 167
  26. lemma OAI.Ostmann.SchwartzCutoff.fourier_psi_at_zero line 176
  27. lemma OAI.Ostmann.SchwartzCutoff.fourier_psi_at_zero_re_pos line 180
  28. theorem OAI.Ostmann.SchwartzCutoff.exists_cutoff line 192