OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPaddedSampling.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The literal padded history table has the same polynomial scalar budget as the supported expansion, and its rational samples approximate the actual full-space history energy.

  1. theorem OAI.ContinuumCoulomb.QuantumPaddedHistory.padded_height line 20
  2. def OAI.ContinuumCoulomb.QuantumPaddedHistory.scalar line 49
  3. theorem OAI.ContinuumCoulomb.QuantumPaddedHistory.scalar_value line 55
  4. theorem OAI.ContinuumCoulomb.QuantumPaddedHistory.scalar_height line 60
  5. def OAI.ContinuumCoulomb.QuantumPaddedHistory.sampledWeight line 78
  6. theorem OAI.ContinuumCoulomb.QuantumPaddedHistory.sampledWeight_bound line 81
  7. theorem OAI.ContinuumCoulomb.QuantumPaddedHistory.sampled_error line 85
  8. theorem OAI.ContinuumCoulomb.QuantumPaddedHistory.sampled_accuracy line 109