OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarResolventTails.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The same sharp exponential rate for compact forcing derivatives. The heat-kernel proof is applied to the actual first/second derivative forcing, without assuming differentiated resolvent asymptotics.

  1. theorem OAI.ContinuumCoulomb.planarResolventOf_product_integrable line 14
  2. theorem OAI.ContinuumCoulomb.planarResolventOf_bounded_heat_representation line 22
  3. theorem OAI.ContinuumCoulomb.planar_supported_exponential_bound line 31
  4. theorem OAI.ContinuumCoulomb.planarHeatOf_tilt_bound line 45
  5. theorem OAI.ContinuumCoulomb.planarResolventOf_tilt_bound line 71
  6. theorem OAI.ContinuumCoulomb.planarResolventOf_sharp_upper line 98
  7. theorem OAI.ContinuumCoulomb.planarResolventMode_partial_sharp_tail line 112
  8. theorem OAI.ContinuumCoulomb.planarResolventMode_partial_partial_sharp_tail line 123