OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRawFamilyProgram.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

The complete finite rational edge list and offset are computed in polynomial time.

  1. theorem OAI.ContinuumCoulomb.QuantumRawExchange.flatten_code_bound line 12
  2. theorem OAI.ContinuumCoulomb.QuantumRawExchange.fold_append line 21
  3. def OAI.ContinuumCoulomb.QuantumRawExchange.flattenProgram line 27
  4. abbrev OAI.ContinuumCoulomb.QuantumRawExchange.FamilyInput line 45
  5. def OAI.ContinuumCoulomb.QuantumRawExchange.familyCode line 46
  6. def OAI.ContinuumCoulomb.QuantumRawExchange.termBondsList line 48
  7. def OAI.ContinuumCoulomb.QuantumRawExchange.termScalarList line 49
  8. def OAI.ContinuumCoulomb.QuantumRawExchange.zeroRaw line 51
  9. opaque OAI.ContinuumCoulomb.QuantumRawExchange.termBondsProgram line 53
  10. opaque OAI.ContinuumCoulomb.QuantumRawExchange.termScalarProgram line 58
  11. abbrev OAI.ContinuumCoulomb.QuantumRawExchange.PenaltyInput line 63
  12. def OAI.ContinuumCoulomb.QuantumRawExchange.penaltyCode line 64
  13. def OAI.ContinuumCoulomb.QuantumRawExchange.penaltyBlock line 66
  14. def OAI.ContinuumCoulomb.QuantumRawExchange.penalty line 70
  15. opaque OAI.ContinuumCoulomb.QuantumRawExchange.penaltyIndexProgram line 72
  16. opaque OAI.ContinuumCoulomb.QuantumRawExchange.penaltyScaleProgram line 74
  17. opaque OAI.ContinuumCoulomb.QuantumRawExchange.penaltyBaseProgram line 75
  18. opaque OAI.ContinuumCoulomb.QuantumRawExchange.penaltyShiftProgram line 77
  19. opaque OAI.ContinuumCoulomb.QuantumRawExchange.penaltySquareProgram line 79
  20. opaque OAI.ContinuumCoulomb.QuantumRawExchange.penaltyBondProgram line 82
  21. opaque OAI.ContinuumCoulomb.QuantumRawExchange.penaltyBlockProgram line 85
  22. opaque OAI.ContinuumCoulomb.QuantumRawExchange.penaltyProgram line 87
  23. abbrev OAI.ContinuumCoulomb.QuantumRawExchange.FullInput line 91
  24. def OAI.ContinuumCoulomb.QuantumRawExchange.fullCode line 92
  25. def OAI.ContinuumCoulomb.QuantumRawExchange.fullBonds line 94
  26. def OAI.ContinuumCoulomb.QuantumRawExchange.fullScalar line 95
  27. opaque OAI.ContinuumCoulomb.QuantumRawExchange.fullCountProgram line 97
  28. opaque OAI.ContinuumCoulomb.QuantumRawExchange.fullFamilyProgram line 98
  29. opaque OAI.ContinuumCoulomb.QuantumRawExchange.fullScaleProgram line 99
  30. opaque OAI.ContinuumCoulomb.QuantumRawExchange.fullPenaltyInputProgram line 101
  31. opaque OAI.ContinuumCoulomb.QuantumRawExchange.fullBondsProgram line 103
  32. opaque OAI.ContinuumCoulomb.QuantumRawExchange.fullCountRatProgram line 106
  33. opaque OAI.ContinuumCoulomb.QuantumRawExchange.fullSixCountProgram line 108
  34. opaque OAI.ContinuumCoulomb.QuantumRawExchange.fullPenaltyScalarProgram line 110
  35. opaque OAI.ContinuumCoulomb.QuantumRawExchange.fullScalarProgram line 112
  36. def OAI.ContinuumCoulomb.QuantumRawExchange.fullCertificate line 115