OAI/Analysis/HotSpots/Potentials.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictHotSpots.Weyl.radialBump line 14
  2. lemma OAI.StrictHotSpots.Weyl.radialBump_contDiff line 16
  3. lemma OAI.StrictHotSpots.Weyl.radialBump_zero line 19
  4. lemma OAI.StrictHotSpots.Weyl.radialBump_support line 24
  5. lemma OAI.StrictHotSpots.Weyl.radialBump_compact line 32
  6. lemma OAI.StrictHotSpots.Weyl.radialBump_integral_pos line 35
  7. lemma OAI.StrictHotSpots.Weyl.radialBump_polar line 46
  8. lemma OAI.StrictHotSpots.Weyl.polar_continuous line 49
  9. lemma OAI.StrictHotSpots.Weyl.polar_circle line 56
  10. lemma OAI.StrictHotSpots.Weyl.angle_integral line 61
  11. lemma OAI.StrictHotSpots.Weyl.polar_bump_integrable line 75
  12. theorem OAI.StrictHotSpots.Weyl.radial_average line 95
  13. lemma OAI.StrictHotSpots.Weyl.convolution_assoc_scalar line 135
  14. lemma OAI.StrictHotSpots.Weyl.convolution_shuffle line 149
  15. theorem OAI.StrictHotSpots.Weyl.local_representative line 174
  16. theorem OAI.StrictHotSpots.Weyl.representative line 214
  17. abbrev OAI.StrictHotSpots.Hodge.e line 264
  18. abbrev OAI.StrictHotSpots.Hodge.c line 265
  19. lemma OAI.StrictHotSpots.Hodge.expand line 267
  20. lemma OAI.StrictHotSpots.Hodge.basis_inner line 269
  21. lemma OAI.StrictHotSpots.Hodge.inner_two line 271
  22. def OAI.StrictHotSpots.Hodge.rot line 275
  23. lemma OAI.StrictHotSpots.Hodge.rot_apply line 277
  24. lemma OAI.StrictHotSpots.Hodge.c_rot line 280
  25. lemma OAI.StrictHotSpots.Hodge.rot_rot line 284
  26. lemma OAI.StrictHotSpots.Hodge.rot_inner line 289
  27. lemma OAI.StrictHotSpots.Hodge.rot_skew line 292
  28. lemma OAI.StrictHotSpots.Hodge.rot_norm line 295
  29. abbrev OAI.StrictHotSpots.Hodge.D line 300
  30. lemma OAI.StrictHotSpots.Hodge.D_smooth line 301
  31. lemma OAI.StrictHotSpots.Hodge.D_compact line 303
  32. lemma OAI.StrictHotSpots.Hodge.D_support line 305
  33. lemma OAI.StrictHotSpots.Hodge.gradient_c line 307
  34. lemma OAI.StrictHotSpots.Hodge.D_D line 309
  35. lemma OAI.StrictHotSpots.Hodge.laplace_two line 321
  36. lemma OAI.StrictHotSpots.Hodge.inner_gradient line 326
  37. lemma OAI.StrictHotSpots.Hodge.inner_rot_gradient line 329
  38. def OAI.StrictHotSpots.Weyl.coord line 346
  39. def OAI.StrictHotSpots.Weyl.complexExtension line 348
  40. lemma OAI.StrictHotSpots.Weyl.complexExtension_integral line 351
  41. lemma OAI.StrictHotSpots.Weyl.complexExtension_integrable line 365
  42. lemma OAI.StrictHotSpots.Weyl.complexExtension_weak line 372
  43. theorem OAI.StrictHotSpots.Weyl.plane_representative line 392
  44. structure OAI.StrictHotSpots.Primitives.DiscreteReal line 422
  45. instance OAI.StrictHotSpots.Primitives.(instance at line 425) line 425
  46. instance OAI.StrictHotSpots.Primitives.(instance at line 426) line 426
  47. lemma OAI.StrictHotSpots.Primitives.DiscreteReal.ext line 428
  48. structure OAI.StrictHotSpots.Primitives.Atlas line 434
  49. def OAI.StrictHotSpots.Primitives.Atlas.core line 446
  50. theorem OAI.StrictHotSpots.Primitives.Atlas.exists_locally_potential line 481
  51. theorem OAI.StrictHotSpots.Primitives.exists_primitive line 529
  52. def OAI.StrictHotSpots.Truncation.trunc line 586
  53. lemma OAI.StrictHotSpots.Truncation.smooth line 587
  54. lemma OAI.StrictHotSpots.Truncation.derivative line 589
  55. lemma OAI.StrictHotSpots.Truncation.deriv_bound line 595
  56. lemma OAI.StrictHotSpots.Truncation.norm_le line 598
  57. lemma OAI.StrictHotSpots.Truncation.bounded line 603
  58. lemma OAI.StrictHotSpots.Truncation.tends line 608
  59. lemma OAI.StrictHotSpots.anchored_l2_bound line 633
  60. theorem OAI.StrictHotSpots.finiteEnergy_hasH1Gradient line 679
  61. theorem OAI.StrictHotSpots.closed_finiteEnergy_potential line 774
  62. theorem OAI.StrictHotSpots.closed_orthogonal_gradient_zero line 809
  63. def OAI.StrictHotSpots.Hodge.WeakDivZero line 838
  64. def OAI.StrictHotSpots.Hodge.WeakCurlZero line 842
  65. lemma OAI.StrictHotSpots.Hodge.weak_harmonic_coordinates line 846
  66. theorem OAI.StrictHotSpots.Hodge.weak_divCurl_smooth line 877
  67. lemma OAI.StrictHotSpots.Hodge.smooth_curl_zero line 889
  68. lemma OAI.StrictHotSpots.Hodge.smooth_closed line 927
  69. theorem OAI.StrictHotSpots.Hodge.weak_divCurl_zero line 960