OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/WeakComplexLaplacian.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Integration by parts for a complex C2 orbital against the full weak-H1 space. Only the sum of its second derivatives is required to lie in L2.

  1. def OAI.ContinuumCoulomb.configurationComplexPartial line 13
  2. def OAI.ContinuumCoulomb.configurationComplexLaplacian line 17
  3. theorem OAI.ContinuumCoulomb.configurationComplexPartial_C1 line 21
  4. theorem OAI.ContinuumCoulomb.h1_inner_complex_coordinate line 26
  5. theorem OAI.ContinuumCoulomb.weakH1_complex_laplacian_pairing line 37