OAI/Analysis/AncientFlat/Spectral/ResolventCoefficients.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PeriodicResolvent.osc_periodic line 9
  2. lemma OAI.PeriodicResolvent.osc_smooth line 15
  3. lemma OAI.PeriodicResolvent.freq_ne_zero line 18
  4. lemma OAI.PeriodicResolvent.coeff_const line 22
  5. lemma OAI.PeriodicResolvent.coeff_map line 31
  6. lemma OAI.PeriodicResolvent.coeff_sub line 38
  7. lemma OAI.PeriodicResolvent.coeff_smul line 44
  8. lemma OAI.PeriodicResolvent.coeff_shift line 48
  9. def OAI.PeriodicResolvent.resolventLoop line 52
  10. lemma OAI.PeriodicResolvent.loop_smooth line 54
  11. lemma OAI.PeriodicResolvent.loop_periodic line 70
  12. lemma OAI.PeriodicResolvent.loop_identity line 75
  13. theorem OAI.PeriodicResolvent.green_summable line 85
  14. lemma OAI.PeriodicResolvent.green_identity line 89