OAI/Analysis/ModularRecovery/FourierOperators.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Normalized Fourier operators, Schwarz inequalities, and multiplication.

  1. lemma OAI.BoundedRecovery.StandardModularData.exists_fourierKernel_lift line 19
  2. def OAI.BoundedRecovery.StandardModularData.fourierKernel line 32
  3. lemma OAI.BoundedRecovery.StandardModularData.fourierKernel_xi line 37
  4. lemma OAI.BoundedRecovery.StandardModularData.norm_fourierKernel_le line 43
  5. lemma OAI.BoundedRecovery.StandardModularData.fourierKernel_strong_tendsto line 47
  6. lemma OAI.BoundedRecovery.StandardModularData.fourierKernel_add line 57
  7. lemma OAI.BoundedRecovery.StandardModularData.fourierKernel_smul line 67
  8. lemma OAI.BoundedRecovery.StandardModularData.fourierKernel_one line 78
  9. lemma OAI.BoundedRecovery.StandardModularData.fourierKernel_star line 86
  10. lemma OAI.BoundedRecovery.StandardModularData.fourierKernel_gram_vector_nonneg line 101
  11. def OAI.BoundedRecovery.StandardModularData.normalizedFourier line 127
  12. lemma OAI.BoundedRecovery.StandardModularData.normalizedFourier_add line 131
  13. lemma OAI.BoundedRecovery.StandardModularData.normalizedFourier_smul line 136
  14. lemma OAI.BoundedRecovery.StandardModularData.normalizedFourier_star line 141
  15. lemma OAI.BoundedRecovery.StandardModularData.normalizedFourier_one line 146
  16. lemma OAI.BoundedRecovery.StandardModularData.normalizedFourier_xi line 150
  17. lemma OAI.BoundedRecovery.StandardModularData.kernelFourier_ne_zero line 157
  18. lemma OAI.BoundedRecovery.StandardModularData.normalizedFourier_gram_vector_nonneg line 162
  19. lemma OAI.BoundedRecovery.StandardModularData.normalizedFourier_schwarz line 183
  20. lemma OAI.BoundedRecovery.StandardModularData.phi_normalizedFourier line 217
  21. lemma OAI.BoundedRecovery.StandardModularData.phi_faithful_nonneg line 233
  22. lemma OAI.BoundedRecovery.StandardModularData.normalizedFourier_star_square line 238
  23. lemma OAI.BoundedRecovery.sesq_zero_of_diagonal line 263
  24. lemma OAI.BoundedRecovery.StandardModularData.normalizedFourier_star_mul line 284
  25. lemma OAI.BoundedRecovery.StandardModularData.normalizedFourier_mul line 310