OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPaddedLocal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact full-space meaning of a fixed-width local coefficient table. The coordinate map is the order of the literal support list; padding only duplicates local words and never introduces spectator configurations.

  1. def OAI.ContinuumCoulomb.QuantumPaddedLocal.reindex line 16
  2. def OAI.ContinuumCoulomb.QuantumPaddedLocal.word line 21
  3. theorem OAI.ContinuumCoulomb.QuantumPaddedLocal.word_support line 25
  4. theorem OAI.ContinuumCoulomb.QuantumPaddedLocal.yCount_reindex line 29
  5. theorem OAI.ContinuumCoulomb.QuantumPaddedLocal.word_even line 42
  6. theorem OAI.ContinuumCoulomb.QuantumPaddedLocal.local_word line 48
  7. theorem OAI.ContinuumCoulomb.QuantumPaddedLocal.local_expansion line 56
  8. theorem OAI.ContinuumCoulomb.QuantumPaddedLocal.full_expansion line 69