OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ClassicalH1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

C1 functions with square-integrable classical partials belong to the actual weak H1 domain. Only the test function needs compact support; this allows the decaying manufactured orbitals and their finite Slater sums.

  1. theorem OAI.ContinuumCoulomb.complex_C1_test_ibp line 14
  2. def OAI.ContinuumCoulomb.classicalH1State line 37