OAI/Analysis/AncientFlat/Kernel/FourierDecay.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicResolvent.freq line 9
  2. def OAI.PeriodicResolvent.osc line 10
  3. lemma OAI.PeriodicResolvent.osc_continuous line 11
  4. lemma OAI.PeriodicResolvent.osc_deriv line 14
  5. lemma OAI.PeriodicResolvent.osc_norm line 19
  6. lemma OAI.PeriodicResolvent.osc_zero line 21
  7. lemma OAI.PeriodicResolvent.osc_one line 22
  8. lemma OAI.PeriodicResolvent.osc_add line 28
  9. def OAI.PeriodicResolvent.coeff line 34
  10. lemma OAI.PeriodicResolvent.coeff_derivative line 35
  11. lemma OAI.PeriodicResolvent.periodic_deriv line 47
  12. lemma OAI.PeriodicResolvent.coeff_norm_le line 55
  13. lemma OAI.PeriodicResolvent.freq_sq_ge line 65
  14. theorem OAI.PeriodicResolvent.summable_coeff_norm line 72