OAI/Analysis/CoulombIonization/Variational/SpatialRotation.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CoulombAtom.SpatialRotation line 142
  2. instance OAI.CoulombAtom.spatialOperatorContinuousStar line 144
  3. instance OAI.CoulombAtom.spatialRotationCompact line 147
  4. instance OAI.CoulombAtom.spatialRotationMeasurable line 154
  5. instance OAI.CoulombAtom.spatialRotationBorel line 155
  6. def OAI.CoulombAtom.rotationMeasure line 157
  7. instance OAI.CoulombAtom.rotationMeasureProbability line 159
  8. instance OAI.CoulombAtom.rotationMeasureLeftInvariant line 163
  9. def OAI.CoulombAtom.rotate line 166
  10. lemma OAI.CoulombAtom.rotate_continuous line 168
  11. lemma OAI.CoulombAtom.rotate_mul line 171
  12. lemma OAI.CoulombAtom.rotate_one line 174
  13. lemma OAI.CoulombAtom.exists_rotate_norm_eq line 176
  14. lemma OAI.CoulombAtom.rotation_integral_left line 181
  15. lemma OAI.CoulombAtom.packetDensity_rotate line 185
  16. lemma OAI.CoulombAtom.packetDensity_joint_continuous line 190
  17. def OAI.CoulombAtom.averagedPacket line 196
  18. lemma OAI.CoulombAtom.averagedPacket_radial line 199
  19. lemma OAI.CoulombAtom.averagedPacket_support line 208
  20. lemma OAI.CoulombAtom.rotationalPacket_continuous line 222
  21. lemma OAI.CoulombAtom.averagedPacket_continuous line 230
  22. lemma OAI.CoulombAtom.averagedPacket_compact line 245
  23. lemma OAI.CoulombAtom.rotationalPacket_compact line 251
  24. lemma OAI.CoulombAtom.rotationalPacket_integrable line 262
  25. lemma OAI.CoulombAtom.averagedPacket_mass line 267
  26. lemma OAI.CoulombAtom.averagedPacket_integrable line 273
  27. lemma OAI.CoulombAtom.averagedPacket_memLp line 277
  28. lemma OAI.CoulombAtom.packetDensity_nonneg line 281
  29. lemma OAI.CoulombAtom.averagedPacket_nonneg line 285