OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFourTensorForms.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The full physical quadratic form in its actual encoded and orthogonal coordinates.

  1. theorem OAI.ContinuumCoulomb.qmaFourTensor_inclusion_norm line 13
  2. theorem OAI.ContinuumCoulomb.qmaFourTensor_norm_decomposition line 18
  3. theorem OAI.ContinuumCoulomb.qmaFourTensorHigh_norm line 24
  4. theorem OAI.ContinuumCoulomb.qmaFourTensorHigh_fixed line 33
  5. theorem OAI.ContinuumCoulomb.qmaFourTensorHigh_symmetric line 38
  6. theorem OAI.ContinuumCoulomb.qmaFourTensor_penalty_low line 43
  7. theorem OAI.ContinuumCoulomb.qmaFourTensor_padded_high line 50
  8. def OAI.ContinuumCoulomb.qmaFourTensorPhysical line 61
  9. def OAI.ContinuumCoulomb.qmaFourTensorLow line 65
  10. def OAI.ContinuumCoulomb.qmaFourTensorOff line 69
  11. def OAI.ContinuumCoulomb.qmaFourTensorHighPerturbation line 73
  12. theorem OAI.ContinuumCoulomb.qmaFourTensorPhysical_symmetric line 77
  13. theorem OAI.ContinuumCoulomb.qmaFourTensorPhysical_low line 87
  14. theorem OAI.ContinuumCoulomb.qmaFourTensorPhysical_high line 101
  15. theorem OAI.ContinuumCoulomb.qmaFourTensorPhysical_energy line 112