OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/WeakH1Pairing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Integration by parts against a noncompact square-integrable C1 function on the actual weak-H1 graph. Compact approximation is used only through the explicit published Sobolev density input.

  1. theorem OAI.ContinuumCoulomb.complex_C1_compact_test_ibp line 15
  2. theorem OAI.ContinuumCoulomb.h1_inner_real_coordinate line 30
  3. theorem OAI.ContinuumCoulomb.weakH1_real_test_ibp line 43