OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/RealMollification.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Smooth approximation of real L² functions on the actual configuration space. Fatou and the contraction estimate suffice; no Sobolev density input is used. This is the scalar approximation needed for the H=W discharge.

  1. theorem OAI.ContinuumCoulomb.l2_error_eventually_lt line 15
  2. def OAI.ContinuumCoulomb.realMollification line 58
  3. theorem OAI.ContinuumCoulomb.realMollification_smooth line 61
  4. theorem OAI.ContinuumCoulomb.realMollification_contraction line 67
  5. theorem OAI.ContinuumCoulomb.realMollification_error line 81