OAI/Analysis/NodalLength/Parametrix.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpNodal.Profiles.parametrixCutoff line 98
  2. def OAI.SharpNodal.Profiles.parametrixInner line 99
  3. def OAI.SharpNodal.Profiles.parametrixSmoothLog line 100
  4. def OAI.SharpNodal.Profiles.parametrixCorrection line 102
  5. def OAI.SharpNodal.Profiles.parametrixKernel line 103
  6. def OAI.SharpNodal.Profiles.logParametrix line 104
  7. lemma OAI.SharpNodal.Profiles.smooth_parametrixSmoothLog line 106
  8. lemma OAI.SharpNodal.Profiles.smooth_parametrixCorrection line 119
  9. lemma OAI.SharpNodal.Profiles.smooth_parametrixKernel line 121
  10. lemma OAI.SharpNodal.Profiles.parametrixSmoothLog_eq line 123
  11. lemma OAI.SharpNodal.Profiles.logParametrix_eq line 129
  12. lemma OAI.SharpNodal.Profiles.laplacian_of_log_germ line 137
  13. lemma OAI.SharpNodal.Profiles.parametrixKernel_zero line 155
  14. lemma OAI.SharpNodal.Profiles.compact_parametrixKernel line 166
  15. lemma OAI.SharpNodal.Profiles.logParametrix_zero line 171
  16. lemma OAI.SharpNodal.Profiles.integral_parametrix_identity line 175
  17. def OAI.SharpNodal.Profiles.rconv line 200
  18. lemma OAI.SharpNodal.Profiles.rconv_eq line 201
  19. lemma OAI.SharpNodal.Profiles.rconv_swap line 202
  20. lemma OAI.SharpNodal.Profiles.smooth_rconv line 205
  21. lemma OAI.SharpNodal.Profiles.partial_rconv line 209
  22. lemma OAI.SharpNodal.Profiles.laplacian_rconv line 222
  23. lemma OAI.SharpNodal.Profiles.partial_reflection line 234
  24. lemma OAI.SharpNodal.Profiles.laplacian_reflection line 246
  25. lemma OAI.SharpNodal.Profiles.compact_reflection line 256
  26. lemma OAI.SharpNodal.Profiles.integrable_logParametrix line 271
  27. lemma OAI.SharpNodal.Profiles.compact_logParametrix line 285
  28. lemma OAI.SharpNodal.Profiles.laplacian_parametrix_convolution line 291
  29. lemma OAI.SharpNodal.Profiles.parametrix_convolution_support line 298
  30. lemma OAI.SharpNodal.Profiles.rconv_duality line 335
  31. lemma OAI.SharpNodal.Profiles.norm_rconv_le line 360
  32. def OAI.SharpNodal.Profiles.WeakHarmonicOn line 381
  33. def OAI.SharpNodal.Profiles.weylRepresentative line 385
  34. lemma OAI.SharpNodal.Profiles.smooth_weylRepresentative line 388
  35. lemma OAI.SharpNodal.Profiles.weylRepresentative_test line 394
  36. lemma OAI.SharpNodal.Profiles.weylRepresentative_ae line 420
  37. lemma OAI.SharpNodal.Profiles.weakHarmonic_smooth line 436
  38. lemma OAI.SharpNodal.Profiles.weylRepresentative_harmonic line 452
  39. lemma OAI.SharpNodal.Profiles.partial_weylRepresentative line 476
  40. lemma OAI.SharpNodal.Profiles.partial2_weylRepresentative line 484
  41. lemma OAI.SharpNodal.Profiles.uniform_weyl_derivative_bounds line 495