TorusHeatInput.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The isotropic two-dimensional periodic heat kernel and its Gaussian bound.

P. Maheux, Notes on Heat Kernels on Infinite dimensional Torus (16 February 2008), Sections 2.1 and 3.1, and Theorem 3.1, equation (3.15), pp. 5, 10--11. The isotropic two-dimensional kernel is rescaled from period 2π to period one. Its generator is the coordinate Laplacian, and its Gaussian estimate is the first upper bound in (3.15). Source: https://idpoisson.fr/maheux/InfiniteTorusV2.pdf

def OAI.ForcedComputation.VelocityDetector.torusDistanceSq line 22
Source documentation
Squared Euclidean distance to the nearest lattice point, using the centered representative in each coordinate.
```
def torusDistanceSq (x : Plane) : ℝ :=
…
```
def OAI.ForcedComputation.VelocityDetector.torusHeatKernel line 25
def OAI.ForcedComputation.VelocityDetector.torusHeatEvolution line 29
structure OAI.ForcedComputation.VelocityDetector.TorusHeatInput line 34
Source documentation
The flat-torus specialization of the heat representation and Gaussian bound.
```
structure TorusHeatInput : Prop where
…
```
theorem OAI.ForcedComputation.VelocityDetector.torusDistanceSq_nonneg line 44
theorem OAI.ForcedComputation.VelocityDetector.torusHeatKernel_nonneg line 47