OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSpatialModel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Spatial data for the actual finite real Hamiltonian, including bounded density.

  1. structure OAI.ContinuumCoulomb.QMASpatialModel line 11
  2. def OAI.ContinuumCoulomb.qmaSpatialHistoryModel line 20