OAI/MathematicalPhysics/DefocusingNLS/Certificates/ScaledLatticeKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A lattice sampling bound uniform as the mesh tends to zero

The exact Cauchy-kernel integral and the integral test give a one-dimensional bound. A twelve-coordinate product then controls the radial kernel.

  1. def OAI.DefocusingNLS.scaledCauchyKernel line 17
  2. theorem OAI.DefocusingNLS.scaledCauchyKernel_nonneg line 19
  3. theorem OAI.DefocusingNLS.scaledCauchyKernel_even line 23
  4. theorem OAI.DefocusingNLS.scaledCauchyKernel_antitone line 26
  5. theorem OAI.DefocusingNLS.scaledCauchyKernel_integrable line 35
  6. theorem OAI.DefocusingNLS.integral_scaledCauchyKernel line 41
  7. theorem OAI.DefocusingNLS.scaledCauchyKernel_integer_sum line 46
  8. theorem OAI.DefocusingNLS.scaled_frequencyCoordinates_injective line 77
  9. theorem OAI.DefocusingNLS.sum_scaledCauchyKernel_product line 85
  10. theorem OAI.DefocusingNLS.scaledRadialKernel_le_product line 115
  11. theorem OAI.DefocusingNLS.scaledRadialKernel_sum line 142