OAI/MathematicalPhysics/BFSS/RellichSmoothing.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Translation estimates and compact smoothing of vector-valued functions.

  1. lemma OAI.BFSSRellich.norm_integral_sq_le line 14
  2. abbrev OAI.BFSSRellich.unitInterval line 22
  3. instance OAI.BFSSRellich.(instance at line 24) line 24
  4. lemma OAI.BFSSRellich.integral_fderiv_segment line 27
  5. lemma OAI.BFSSRellich.translation_pointwise line 42
  6. abbrev OAI.BFSSRellich.Euclidean line 68
  7. lemma OAI.BFSSRellich.continuous_norm_sq_integrable line 70
  8. lemma OAI.BFSSRellich.derivative_norm_sq_integrable line 79
  9. lemma OAI.BFSSRellich.translation_integral_bound line 84
  10. lemma OAI.BFSSRellich.translate_integrable_product line 121
  11. lemma OAI.BFSSRellich.first_integrable_product line 138
  12. lemma OAI.BFSSRellich.norm_sub_sq_le line 149
  13. lemma OAI.BFSSRellich.translate_sub_square_integrable_product line 154
  14. def OAI.BFSSRellich.smoothAverage line 166
  15. lemma OAI.BFSSRellich.smoothAverage_sub_eq line 169
  16. lemma OAI.BFSSRellich.smoothAverage_Jensen line 179
  17. lemma OAI.BFSSRellich.smoothAverage_sub_square_integrable line 199
  18. theorem OAI.BFSSRellich.smoothAverage_error line 213
  19. def OAI.BFSSRellich.kernelAverage line 242
  20. lemma OAI.BFSSRellich.kernel_integrable line 246
  21. lemma OAI.BFSSRellich.kernelAverage_bound line 258
  22. lemma OAI.BFSSRellich.kernelAverage_lipschitz line 273
  23. def OAI.BFSSRellich.bumpMeasure line 313
  24. instance OAI.BFSSRellich.bumpMeasure_probability line 316
  25. lemma OAI.BFSSRellich.bumpMeasure_supported line 324
  26. lemma OAI.BFSSRellich.kernelAverage_eq_smoothAverage line 334
  27. theorem OAI.BFSSRellich.kernelAverage_error line 344