OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFourTensorHilbert.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Actual low/high coordinates and the bounded padded inverse for the four-spin code.

  1. def OAI.ContinuumCoulomb.qmaFourTensorInclusion line 14
  2. def OAI.ContinuumCoulomb.qmaFourTensorRestriction line 18
  3. def OAI.ContinuumCoulomb.qmaFourTensorHigh line 22
  4. theorem OAI.ContinuumCoulomb.qmaFourTensor_restrict_include line 26
  5. theorem OAI.ContinuumCoulomb.qmaFourTensor_inclusion_adjoint line 33
  6. theorem OAI.ContinuumCoulomb.qmaFourTensor_highPart line 41
  7. theorem OAI.ContinuumCoulomb.qmaFourTensorRestriction_high line 50
  8. theorem OAI.ContinuumCoulomb.qmaFourTensor_projection_star line 55
  9. theorem OAI.ContinuumCoulomb.qmaFourTensor_penalty_star line 59
  10. def OAI.ContinuumCoulomb.qmaFourTensorPaddedMatrix line 71
  11. def OAI.ContinuumCoulomb.qmaFourTensorPadded line 74
  12. theorem OAI.ContinuumCoulomb.qmaFourTensor_padded_gap line 78
  13. theorem OAI.ContinuumCoulomb.qmaFourTensor_inverse_exists line 98