OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/HeatKernelModulus.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Quantitative bounds for the scalar heat-resolvent kernel away from time zero. Every constant is elementary in the cutoff and radius.

  1. def OAI.ContinuumCoulomb.HeatKernelModulus.exponent line 12
  2. def OAI.ContinuumCoulomb.HeatKernelModulus.kernel line 13
  3. theorem OAI.ContinuumCoulomb.HeatKernelModulus.kernel_eq_heat line 15
  4. theorem OAI.ContinuumCoulomb.HeatKernelModulus.exp_nonpositive_lipschitz line 20
  5. theorem OAI.ContinuumCoulomb.HeatKernelModulus.reciprocal_lipschitz line 31
  6. theorem OAI.ContinuumCoulomb.HeatKernelModulus.exponent_nonpositive line 40
  7. theorem OAI.ContinuumCoulomb.HeatKernelModulus.exponent_time_lipschitz line 46
  8. theorem OAI.ContinuumCoulomb.HeatKernelModulus.kernel_nonnegative line 61
  9. theorem OAI.ContinuumCoulomb.HeatKernelModulus.kernel_le_inverse line 65
  10. theorem OAI.ContinuumCoulomb.HeatKernelModulus.kernel_space_lipschitz line 77
  11. theorem OAI.ContinuumCoulomb.HeatKernelModulus.kernel_time_lipschitz line 102