OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarHopping.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The actual positive contact hopping integral. Its Lipschitz control is inherited from the compact forcing through the mass-one resolvent kernel.

  1. theorem OAI.ContinuumCoulomb.forcing_lipschitz_exists line 15
  2. def OAI.ContinuumCoulomb.planarForcingLipschitzConstant line 19
  3. theorem OAI.ContinuumCoulomb.planarForcing_lipschitz line 21
  4. theorem OAI.ContinuumCoulomb.planarResolventMode_integrand_integrable line 24
  5. theorem OAI.ContinuumCoulomb.planarResolventMode_norm_sub line 33
  6. theorem OAI.ContinuumCoulomb.planarResolventMode_lipschitz line 51
  7. def OAI.ContinuumCoulomb.planarHoppingIntegrand line 55
  8. theorem OAI.ContinuumCoulomb.planarHoppingIntegrand_continuous line 58
  9. theorem OAI.ContinuumCoulomb.planarHoppingIntegrand_integrable line 62
  10. theorem OAI.ContinuumCoulomb.planarHoppingIntegrand_nonnegative line 66
  11. def OAI.ContinuumCoulomb.planarHopping line 70
  12. theorem OAI.ContinuumCoulomb.planarHopping_positive line 73
  13. theorem OAI.ContinuumCoulomb.planarAxis_zero_norm line 82
  14. def OAI.ContinuumCoulomb.planarHoppingLipschitzConstant line 85
  15. theorem OAI.ContinuumCoulomb.planarHopping_norm_sub line 91
  16. theorem OAI.ContinuumCoulomb.planarHopping_lipschitz line 122