OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarModeDecay.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

An explicit exponential tail of the actual positive planar mode. Splitting the Gaussian exponent avoids any assumed asymptotics for a special function.

  1. theorem OAI.ContinuumCoulomb.planarHeatKernel_double_time line 12
  2. theorem OAI.ContinuumCoulomb.planarHeatForcing_tail line 21
  3. theorem OAI.ContinuumCoulomb.planarHeatAverage_tail line 47
  4. theorem OAI.ContinuumCoulomb.planar_heat_tail_exponent line 56
  5. theorem OAI.ContinuumCoulomb.planarHeatResolvent_tail line 64
  6. theorem OAI.ContinuumCoulomb.planarResolventMode_exponential_tail line 79