OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryThreeLocalEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Full-space energy comparison for the literal three-local history family.

  1. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.familyBottom_instances line 11
  2. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.normalizedBottom_instances line 23
  3. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.bottomError_instances line 31
  4. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.threeLocal_energy_eq line 38
  5. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.sampledHistory_energy_eq line 47
  6. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.history_twoStage_error line 54
  7. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.threeLocal_sampled_error line 67
  8. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.sampledHistory_error line 74
  9. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.threeLocal_accuracy line 79