OAI/Analysis/ModularRecovery/StrongLimits.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Strong spectral limits and orbit limits.

  1. lemma OAI.BoundedRecovery.RealSpectralCalculus.tendsto_calculus_of_compact line 19
  2. lemma OAI.BoundedRecovery.RealSpectralCalculus.kernelMultiplier_strong_tendsto line 66
  3. lemma OAI.BoundedRecovery.StandardModularData.tendsto_apply_of_tendsto_xi line 84
  4. lemma OAI.BoundedRecovery.kernelFourier_star line 136
  5. lemma OAI.BoundedRecovery.kernelFourier_eq_real line 144
  6. lemma OAI.BoundedRecovery.kernelFourier_positive_near_zero line 147