OAI/Analysis/ModularRecovery/GaussianAverages.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Gaussian operator averages and their positivity and adjoint identities.

  1. lemma OAI.BoundedRecovery.spectralCharacter_arg_add line 17
  2. lemma OAI.BoundedRecovery.spectralCharacter_arg_neg line 21
  3. lemma OAI.BoundedRecovery.spectralCharacter_arg_sub line 25
  4. def OAI.BoundedRecovery.gaussianFourierWeight line 29
  5. lemma OAI.BoundedRecovery.integrable_gaussianFourierWeight line 32
  6. lemma OAI.BoundedRecovery.continuous_gaussianFourierWeight line 37
  7. lemma OAI.BoundedRecovery.integrable_weight_translatedKernel line 41
  8. def OAI.BoundedRecovery.kernelMultiplier line 46
  9. lemma OAI.BoundedRecovery.kernelMultiplier_apply line 49
  10. def OAI.BoundedRecovery.StandardModularData.kernelAverageOp line 57
  11. lemma OAI.BoundedRecovery.StandardModularData.kernelAverageOp_mem line 63
  12. def OAI.BoundedRecovery.StandardModularData.kernelAverage line 81
  13. lemma OAI.BoundedRecovery.StandardModularData.kernelAverage_apply line 85
  14. lemma OAI.BoundedRecovery.StandardModularData.kernelAverage_xi line 90
  15. lemma OAI.BoundedRecovery.StandardModularData.kernelAverage_add line 103
  16. lemma OAI.BoundedRecovery.StandardModularData.kernelAverage_smul line 113
  17. lemma OAI.BoundedRecovery.cstarMatrix_vector_nonneg line 133
  18. lemma OAI.BoundedRecovery.StandardModularData.modularGram_vector_nonneg line 157
  19. def OAI.BoundedRecovery.StandardModularData.gramKernelPairing line 173
  20. lemma OAI.BoundedRecovery.StandardModularData.continuous_gramKernelPairing line 177
  21. lemma OAI.BoundedRecovery.StandardModularData.norm_gramKernelPairing_le line 186
  22. lemma OAI.BoundedRecovery.StandardModularData.gramKernelPairing_twisted_positive_definite line 200
  23. lemma OAI.BoundedRecovery.StandardModularData.kernelAverage_gram_vector_nonneg line 231
  24. lemma OAI.BoundedRecovery.gaussianCutoff_even line 289
  25. lemma OAI.BoundedRecovery.gaussianFourierWeight_neg line 292
  26. lemma OAI.BoundedRecovery.StandardModularData.kernelAverage_inner line 301
  27. lemma OAI.BoundedRecovery.StandardModularData.kernelAverage_star line 314