OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FiniteOrbitalLaplacian.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite linear combinations commute with the actual weak-form coordinate Laplacian. These identities are used only for Gram-corrected orbitals.

  1. theorem OAI.ContinuumCoulomb.configurationRealPartial_sum line 12
  2. theorem OAI.ContinuumCoulomb.configurationRealLaplacian_sum line 22