OAI/GroupTheory/Thompson/AnalyticSinc.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The correlation function for the Hilbert-space oscillator

The value at zero is filled in by the derivative of sine. Uniform separation on a positive half-line is proved using one compact interval and the elementary bound on sine, without a limit argument at infinity.

  1. def OAI.ThompsonNonamenability.Analytic.sinc line 23
  2. theorem OAI.ThompsonNonamenability.Analytic.sinc_zero line 25
  3. theorem OAI.ThompsonNonamenability.Analytic.sinc_of_ne_zero line 27
  4. theorem OAI.ThompsonNonamenability.Analytic.sinc_neg line 30
  5. theorem OAI.ThompsonNonamenability.Analytic.sinc_eq_update line 35
  6. theorem OAI.ThompsonNonamenability.Analytic.continuous_sinc line 40
  7. theorem OAI.ThompsonNonamenability.Analytic.abs_sinc_lt_one line 51
  8. theorem OAI.ThompsonNonamenability.Analytic.abs_sinc_le_one line 55
  9. theorem OAI.ThompsonNonamenability.Analytic.sinc_le_one line 60
  10. theorem OAI.ThompsonNonamenability.Analytic.abs_sinc_le_half_of_two_le line 63
  11. theorem OAI.ThompsonNonamenability.Analytic.exists_uniform_sinc_gap line 69