OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/SobolevDensity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The whole-space H=W specialization required by the two continuum reductions. The approximation is constructed by normalized smooth convolution, with no published density hypothesis remaining.

  1. theorem OAI.ContinuumCoulomb.complexMollification_error_tendsto line 14
  2. def OAI.ContinuumCoulomb.mollifiedH1 line 24
  3. theorem OAI.ContinuumCoulomb.mollifiedH1_gradient line 34
  4. theorem OAI.ContinuumCoulomb.mollifiedH1_error_tendsto line 40
  5. theorem OAI.ContinuumCoulomb.publishedSobolevSmoothDensity line 53

    Source documentation

    Meyers–Serrin, H=W, specialized to the full Euclidean weak-H1 space, proved here by the explicit convolution sequence.

    theorem publishedSobolevSmoothDensity : PublishedSobolevSmoothDensity := by
…

    Mentions: OAI.ContinuumCoulomb.PublishedSobolevSmoothDensity