OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarResolvent.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Construction of the actual positive finite-smooth planar resolvent mode. Tonelli/Fubini give an L¹ resolvent kernel of mass one, so convolution with the manuscript's compact forcing has C⁷ regularity. The resolvent differential equation, quantitative tails and excitation gap are subsequent steps.

  1. def OAI.ContinuumCoulomb.planarResolventIntegrand line 18
  2. theorem OAI.ContinuumCoulomb.planarResolventIntegrand_measurable line 21
  3. theorem OAI.ContinuumCoulomb.planarResolventIntegrand_integrable line 25
  4. def OAI.ContinuumCoulomb.planarResolventKernel line 43
  5. theorem OAI.ContinuumCoulomb.planarResolventKernel_integrable line 46
  6. theorem OAI.ContinuumCoulomb.planarResolvent_forcing_integrable line 49
  7. def OAI.ContinuumCoulomb.planarResolventMode line 59
  8. theorem OAI.ContinuumCoulomb.planarResolventMode_C7 line 62
  9. theorem OAI.ContinuumCoulomb.planarResolventMode_heat_representation line 67

    Source documentation

    This is exactly the Gaussian heat representation in the manuscript.

    theorem planarResolventMode_heat_representation (r : PlanarPosition) :
    planarResolventMode r = ∫ t in Set.Ioi (0 : ℝ), Real.exp (-t) * planarHeatAverage t r := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.planarResolventMode, OAI.ContinuumCoulomb.planarHeatAverage

  10. theorem OAI.ContinuumCoulomb.planarResolventMode_heat_integrable line 75
  11. theorem OAI.ContinuumCoulomb.planarResolventMode_positive line 81
  12. theorem OAI.ContinuumCoulomb.planarResolventMode_le_one line 95