GaussianOffDiagonal.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Gaussian decay of the heat kernel away from its pole

def OAI.RegularPointCoordinates.gaussianOffDiagonalEnvelope line 16
Source documentation
The envelope after a polynomial lower bound for small ball volume.
```
def gaussianOffDiagonalEnvelope (s a b t : ℝ) : ℝ :=
…
```
theorem OAI.RegularPointCoordinates.gaussianOffDiagonalEnvelope_nonneg line 19
theorem OAI.RegularPointCoordinates.gaussianOffDiagonalEnvelope_tendsto line 25
Source documentation
Every polynomial volume loss is dominated by a positive off-diagonal Gaussian exponent at small time.
```
theorem gaussianOffDiagonalEnvelope_tendsto (s b : ℝ) {a : ℝ} (ha : 0 < a) :
    Tendsto (gaussianOffDiagonalEnvelope s a b) (𝓝[>] 0) (𝓝 0) := by
…
```
Mentions: OAI.RegularPointCoordinates.gaussianOffDiagonalEnvelope
theorem OAI.RegularPointCoordinates.gaussianOffDiagonalEnvelope_weighted_tendsto line 39
Source documentation
The same error still vanishes after any fixed polynomial loss from an interscale change of normalization.
```
theorem gaussianOffDiagonalEnvelope_weighted_tendsto (s b q : ℝ) {a : ℝ} (ha : 0 < a) :
    Tendsto (fun t : ℝ => (t⁻¹) ^ q * gaussianOffDiagonalEnvelope s a b t)
      (𝓝[>] 0) (𝓝 0) := by
…
```
Mentions: OAI.RegularPointCoordinates.gaussianOffDiagonalEnvelope

theorem OAI.RegularPointCoordinates.gaussian_upper_of_inverse_power_volume line 54

Source documentation

The exact Gaussian upper bound and a lower volume power produce a uniform off-diagonal envelope. The volume hypothesis is in the inverse power form needed here; it is kept separate from the published bound.

theorem gaussian_upper_of_inverse_power_volume
    {t s d C₁ C₂ V ε : ℝ} (ht : 0 < t) (hd : 0 ≤ d)
    (hC : 0 < C₁) (hV : 0 < V) (hden : 0 < 4 + ε) (x y : X)
    (hupper : k t x y ≤ (C₁ / μ.real (ball y (Real.sqrt t))) *
      Real.exp (-(dist x y) ^ 2 / ((4 + ε) * t) + C₂ * t))
    (hvol : V / (t⁻¹) ^ s ≤ μ.real (ball y (Real.sqrt t)))
    (hsep : d ≤ dist x y) :
    k t x y ≤ (C₁ / V) * gaussianOffDiagonalEnvelope s (d ^ 2 / (4 + ε)) C₂ t := by
…

Mentions: OAI.RegularPointCoordinates.gaussianOffDiagonalEnvelope