OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CoreOrbitalProjection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Integrating the one-particle projection estimate over the other electron coordinates. Slices belong to the full weak-H1 domain almost everywhere.

  1. theorem OAI.ContinuumCoulomb.h1_inner_orbital line 14
  2. def OAI.ContinuumCoulomb.coreOrbitalCoefficient line 25
  3. theorem OAI.ContinuumCoulomb.coreOrbitalCoefficient_memLp line 30
  4. theorem OAI.ContinuumCoulomb.core_graphOrbitalMass_ae line 38
  5. theorem OAI.ContinuumCoulomb.core_graphOrbitalMass_integrable line 48
  6. def OAI.ContinuumCoulomb.coreOrbitalMass line 57
  7. theorem OAI.ContinuumCoulomb.coreOrbitalMass_eq_coefficients line 62
  8. theorem OAI.ContinuumCoulomb.bounded_state_potential_integrable line 77
  9. theorem OAI.ContinuumCoulomb.coreOneBody_projection_lower line 88