OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarResolventEquation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The differential eigen-equation of the constructed resolvent mode is obtained from its heat representation and the fundamental theorem of calculus, not supplied as an assumption.

  1. theorem OAI.ContinuumCoulomb.planarResolvent_joint_integrable line 15
  2. theorem OAI.ContinuumCoulomb.planarResolventOf_heat_representation line 26
  3. theorem OAI.ContinuumCoulomb.planarResolventOf_heat_integrable line 35
  4. theorem OAI.ContinuumCoulomb.planarResolventMode_laplacian_integral line 43
  5. def OAI.ContinuumCoulomb.planarHeatResolventPrimitive line 60
  6. def OAI.ContinuumCoulomb.planarHeatResolventDerivative line 63
  7. theorem OAI.ContinuumCoulomb.planarHeatResolventPrimitive_zero line 67
  8. theorem OAI.ContinuumCoulomb.planarHeatResolventPrimitive_hasDerivAt line 71
  9. theorem OAI.ContinuumCoulomb.planarHeatResolventPrimitive_continuousWithinAt line 85
  10. theorem OAI.ContinuumCoulomb.planarHeatResolventDerivative_integrable line 102
  11. theorem OAI.ContinuumCoulomb.planarHeatResolventPrimitive_integrable line 109
  12. theorem OAI.ContinuumCoulomb.planarResolventMode_equation line 115
  13. theorem OAI.ContinuumCoulomb.manufacturedPlanarWell_eigen_equation line 134
  14. theorem OAI.ContinuumCoulomb.manufacturedPlanarWell_test_lower line 142