OAI/Analysis/ModularRecovery/StrongIntegrals.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Strong operator integrals and positivity under Gaussian integration.

  1. lemma OAI.BoundedRecovery.integrable_smul_bounded_orbit line 19
  2. lemma OAI.BoundedRecovery.norm_integral_smul_bounded_orbit line 30
  3. def OAI.BoundedRecovery.strongIntegral line 40
  4. lemma OAI.BoundedRecovery.strongIntegral_apply line 65
  5. lemma OAI.BoundedRecovery.norm_strongIntegral_le line 70
  6. lemma OAI.BoundedRecovery.integral_comp_simple line 87
  7. lemma OAI.BoundedRecovery.integral_positive_kernel line 108
  8. lemma OAI.BoundedRecovery.gaussian_double_sub_integral line 165
  9. lemma OAI.BoundedRecovery.gaussian_positive_definite line 180
  10. def OAI.BoundedRecovery.gaussianCutoff line 196
  11. def OAI.BoundedRecovery.gaussianVariance line 198
  12. def OAI.BoundedRecovery.gaussianNormalization line 200
  13. lemma OAI.BoundedRecovery.gaussianVariance_pos line 203
  14. lemma OAI.BoundedRecovery.gaussianNormalization_pos line 207
  15. lemma OAI.BoundedRecovery.gaussianCutoff_pos line 211
  16. lemma OAI.BoundedRecovery.gaussianCutoff_le_one line 213
  17. lemma OAI.BoundedRecovery.continuous_gaussianCutoff line 217
  18. lemma OAI.BoundedRecovery.integrable_gaussianCutoff line 221
  19. lemma OAI.BoundedRecovery.gaussianCutoff_tendsto line 229
  20. lemma OAI.BoundedRecovery.gaussianNormalization_pdf line 236
  21. lemma OAI.BoundedRecovery.integral_gaussianCutoff_eq line 252
  22. lemma OAI.BoundedRecovery.gaussianCutoff_positive_definite line 260