OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/SplitCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Volume-preserving planar/transverse coordinates for the actual three-dimensional Coulomb space. The intermediate product has its Euclidean L² norm; the final ordinary product carries the same product volume.

  1. def OAI.ContinuumCoulomb.verticalCoordinateEquiv line 14
  2. def OAI.ContinuumCoulomb.positionSplitIsometry line 21
  3. def OAI.ContinuumCoulomb.positionSplitCoordinates line 28
  4. theorem OAI.ContinuumCoulomb.positionSplitCoordinates_measurePreserving line 32
  5. theorem OAI.ContinuumCoulomb.positionSplitCoordinates_integral line 38
  6. theorem OAI.ContinuumCoulomb.positionSplitCoordinates_norm_sq line 43
  7. theorem OAI.ContinuumCoulomb.positionSplitCoordinates_distance line 51
  8. def OAI.ContinuumCoulomb.continuumLocalizedMode line 59
  9. theorem OAI.ContinuumCoulomb.continuumLocalizedMode_C7 line 62
  10. theorem OAI.ContinuumCoulomb.continuumLocalizedMode_positive line 66
  11. theorem OAI.ContinuumCoulomb.continuumLocalizedMode_normalized line 70
  12. theorem OAI.ContinuumCoulomb.continuumLocalizedMode_memLp line 76