OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarNormalizationTail.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Quantitative truncation of the actual planar normalization integral. All constants below depend only on the fixed manufactured forcing.

  1. def OAI.ContinuumCoulomb.planarNormalizationTailConstant line 13
  2. theorem OAI.ContinuumCoulomb.planarNormalizationTailConstant_nonnegative line 17
  3. theorem OAI.ContinuumCoulomb.real_quarter_exponential_integral line 22
  4. theorem OAI.ContinuumCoulomb.planar_half_exponential_integral_le line 29
  5. theorem OAI.ContinuumCoulomb.planarNormalizationTailConstant_le line 63
  6. theorem OAI.ContinuumCoulomb.planarResolvent_square_tail_pointwise line 79
  7. theorem OAI.ContinuumCoulomb.planarNormalization_tail line 95