OAI/Analysis/CoulombRadii/FieldAnalysis/Rotation.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Coulomb.Rotation line 114
  2. lemma OAI.Coulomb.rotation_entry_sq_sum line 116
  3. lemma OAI.Coulomb.rotation_entry_abs_le line 121
  4. lemma OAI.Coulomb.rotation_closed line 127
  5. lemma OAI.Coulomb.rotation_set_compact line 132
  6. instance OAI.Coulomb.rotation_compact line 139
  7. instance OAI.Coulomb.rotation_continuousStar line 142
  8. instance OAI.Coulomb.rotation_continuousInv line 144
  9. instance OAI.Coulomb.rotation_topologicalGroup line 146
  10. instance OAI.Coulomb.rotation_measurable line 148
  11. instance OAI.Coulomb.rotation_borel line 149
  12. def OAI.Coulomb.rotationMeasure line 151
  13. instance OAI.Coulomb.(instance at line 154) line 154
  14. def OAI.Coulomb.rotationIsometry line 156
  15. lemma OAI.Coulomb.rotationIsometry_apply line 164
  16. lemma OAI.Coulomb.rotationIsometry_measurePreserving line 167
  17. lemma OAI.Coulomb.rotation_action_continuous line 171
  18. lemma OAI.Coulomb.flatFineKernel_continuous line 184
  19. lemma OAI.Coulomb.flatFineKernel_le line 190
  20. lemma OAI.Coulomb.flatFineKernel_eq_zero line 200
  21. def OAI.Coulomb.fineKernel line 217
  22. lemma OAI.Coulomb.rotated_flatKernel_continuous line 220
  23. lemma OAI.Coulomb.rotated_flatKernel_integrable line 224
  24. lemma OAI.Coulomb.fineKernel_nonneg line 229
  25. lemma OAI.Coulomb.fineKernel_le line 232
  26. lemma OAI.Coulomb.fineKernel_eq_zero line 239
  27. lemma OAI.Coulomb.rotationIsometry_mul line 248
  28. instance OAI.Coulomb.(instance at line 256) line 256
  29. instance OAI.Coulomb.(instance at line 260) line 260
  30. instance OAI.Coulomb.(instance at line 264) line 264
  31. lemma OAI.Coulomb.fineKernel_rotation line 276
  32. lemma OAI.Coulomb.tent_continuous line 282
  33. lemma OAI.Coulomb.tent_eq_zero line 283
  34. lemma OAI.Coulomb.tent_integrable line 289
  35. lemma OAI.Coulomb.tent_integral line 299
  36. lemma OAI.Coulomb.flatFineKernel_integrable line 325
  37. lemma OAI.Coulomb.flatFineKernel_integral line 328
  38. lemma OAI.Coulomb.flatFineKernel_space_integrable line 337
  39. lemma OAI.Coulomb.flatFineKernel_space_integral line 341
  40. lemma OAI.Coulomb.rotated_flatKernel_space_integrable line 346
  41. lemma OAI.Coulomb.rotated_flatKernel_space_integral line 350
  42. lemma OAI.Coulomb.rotated_flatKernel_integrable_prod line 356
  43. lemma OAI.Coulomb.fineKernel_integrable line 366
  44. lemma OAI.Coulomb.fineKernel_integral line 369
  45. lemma OAI.Coulomb.rpow_five_thirds_le_linear line 375
  46. lemma OAI.Coulomb.fineKernel_measurable line 382
  47. def OAI.Coulomb.fineDensity line 385
  48. def OAI.Coulomb.rotatedFlatDensity line 387
  49. lemma OAI.Coulomb.fineDensity_nonneg line 390
  50. lemma OAI.Coulomb.fineDensity_le line 392
  51. lemma OAI.Coulomb.rotatedFlatDensity_nonneg line 397
  52. lemma OAI.Coulomb.rotatedFlatDensity_le line 399
  53. lemma OAI.Coulomb.fineDensity_measurable line 405
  54. lemma OAI.Coulomb.rotatedFlatDensity_continuous line 409
  55. lemma OAI.Coulomb.fineDensity_integrable line 419
  56. lemma OAI.Coulomb.fineDensity_integral line 425
  57. lemma OAI.Coulomb.rotatedFlatDensity_integrable line 434
  58. lemma OAI.Coulomb.rotatedFlatDensity_integral line 441
  59. lemma OAI.Coulomb.rotatedFlatDensity_power_integrable line 455
  60. lemma OAI.Coulomb.rotatedFlatDensity_power_integral_le line 463
  61. lemma OAI.Coulomb.rotatedFlatDensity_power_integrable_prod line 472
  62. lemma OAI.Coulomb.fineDensity_eq_angularAverage line 486
  63. lemma OAI.Coulomb.rotatedFlatDensity_angular_integrable line 491
  64. lemma OAI.Coulomb.rotatedFlatDensity_power_angular_integrable line 495
  65. lemma OAI.Coulomb.fineDensity_Jensen line 503
  66. def OAI.Coulomb.fineDensityPower line 512
  67. lemma OAI.Coulomb.fineDensityPower_le_angularAverage line 515
  68. lemma OAI.Coulomb.rotatedFlatDensityPower_eq line 526