GaussianHeatInput.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The quantitative published heat-kernel input

Jiang--Li--Zhang (2016), Theorem 1.2, gives these two Gaussian bounds on RCD*(K,N) spaces for K < 0. We use only 0 < ε < 1 and finite-dimensional noncollapsed spaces. Source: https://arxiv.org/pdf/1407.5289v2 .

def OAI.RegularPointCoordinates.HasGaussianHeatBounds line 27
Source documentation
The pair of Gaussian bounds, with the measure at the kernel's second argument and the exact 4 ± ε denominators.
```
def HasGaussianHeatBounds : Prop :=
…
```

theorem OAI.RegularPointCoordinates.gaussian_lower_on_set line 37

Source documentation

A Gaussian lower bound becomes uniform on any testing set where the distance and local ball volumes have the stated uniform bounds.

theorem gaussian_lower_on_set {s : Set X} {t ε C₁ C₂ A V : ℝ}
    (ht : 0 < t) (hε : ε < 1) (hC : 0 < C₁)
    (x : X)
    (hlower : ∀ y ∈ s,
      (C₁ * μ.real (Metric.ball y (Real.sqrt t)))⁻¹ *
        Real.exp (-(dist x y) ^ 2 / ((4 - ε) * t) - C₂ * t) ≤ p t x y)
    (hvolume : ∀ y ∈ s, 0 < μ.real (Metric.ball y (Real.sqrt t)) ∧
      μ.real (Metric.ball y (Real.sqrt t)) ≤ V)
    (hdist : ∀ y ∈ s, (dist x y) ^ 2 ≤ A * t) :
    ∀ y ∈ s, (C₁ * V)⁻¹ * Real.exp (-A / (4 - ε) - C₂ * t) ≤ p t x y := by
…

theorem OAI.RegularPointCoordinates.HasGaussianHeatBounds.exists_heatGram_lower_mean line 72

Source documentation

The cited Gaussian estimate supplies the lower comparison for the actual cutoff heat Gram on any fixed ball satisfying volume bounds. The positive constant is chosen before the coefficient vector.

theorem HasGaussianHeatBounds.exists_heatGram_lower_mean
    (hg : HasGaussianHeatBounds μ p) (hp : IsContinuousHeatKernel μ hQ p)
    {χ : X → ℝ} (hχ : Continuous χ) (hsχ : HasCompactSupport χ)
    (U : E →L[ℝ] SobolevSpace μ hQ) (s : Set X) (hs : MeasurableSet s)
    (hμ : 0 < μ.real s) (hχpos : ∀ y, 0 ≤ χ y) (hχone : ∀ y ∈ s, χ y = 1)
    {t : ℝ} (ht : 0 < t) (x : X) {V A lambda : ℝ} (hV : 0 < V)
    (hlambda : 0 ≤ lambda)
    (hvolume : ∀ y ∈ s, 0 < μ.real (Metric.ball y (Real.sqrt t)) ∧
      μ.real (Metric.ball y (Real.sqrt t)) ≤ V)
    (hdist : ∀ y ∈ s, (dist x y) ^ 2 ≤ A * t) :
    ∃ c : ℝ, 0 < c ∧ ∀ v : E,
      c * ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ ≤
…

Mentions: OAI.RegularPointCoordinates.HasGaussianHeatBounds, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.sobolevMeanGram

theorem OAI.RegularPointCoordinates.HasGaussianHeatBounds.exists_heatGram_mass_lower line 100

Source documentation

One Gaussian constant controls both actual Gram energy and the full local mass measure. This is the common lower bound used when heat decrements are compared to normalized ball masses.

theorem HasGaussianHeatBounds.exists_heatGram_mass_lower
    [FiniteDimensional ℝ E]
    (hg : HasGaussianHeatBounds μ p) (hp : IsContinuousHeatKernel μ hQ p)
    {χ : X → ℝ} (hχ : Continuous χ) (hsχ : HasCompactSupport χ)
    (U : E →L[ℝ] SobolevSpace μ hQ) (M : PositiveBilinearMeasure X E)
    (s : Set X) (hs : MeasurableSet s) (hμ : 0 < μ.real s)
    (hχpos : ∀ y, 0 ≤ χ y) (hχone : ∀ y ∈ s, χ y = 1)
    {t : ℝ} (ht : 0 < t) (x : X) {V A lambda : ℝ} (hV : 0 < V)
    (hlambda : 0 ≤ lambda)
    (hvolume : ∀ y ∈ s, 0 < μ.real (Metric.ball y (Real.sqrt t)) ∧
      μ.real (Metric.ball y (Real.sqrt t)) ≤ V)
    (hdist : ∀ y ∈ s, (dist x y) ^ 2 ≤ A * t) :
…

Mentions: OAI.RegularPointCoordinates.HasGaussianHeatBounds, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure