OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Scalar/TorusHeatGaussianBound.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Elementary lattice estimates for the two-dimensional torus heat kernel.

  1. theorem OAI.ForcedComputation.VelocityDetector.gaussian_nat_tsum_le line 13
  2. theorem OAI.ForcedComputation.VelocityDetector.gaussianLattice_add_int line 27
  3. theorem OAI.ForcedComputation.VelocityDetector.gaussianLattice_neg line 39
  4. theorem OAI.ForcedComputation.VelocityDetector.gaussianLattice_abs line 50
  5. theorem OAI.ForcedComputation.VelocityDetector.gaussian_nat_summable line 55
  6. theorem OAI.ForcedComputation.VelocityDetector.gaussian_nat_scaled_le line 61
  7. theorem OAI.ForcedComputation.VelocityDetector.gaussianLattice_centered_le line 69
  8. theorem OAI.ForcedComputation.VelocityDetector.gaussianLattice_nearest_le line 123
  9. theorem OAI.ForcedComputation.VelocityDetector.gaussianLattice_nonneg line 143
  10. theorem OAI.ForcedComputation.VelocityDetector.torusHeatKernel_gaussian line 146