ActualHeatGrams.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Heat averages of the canonical Sobolev Gram form

The published kernel input is the specialization of Jiang--Li--Zhang, Heat kernel bounds on metric measure spaces and some applications (2016), Section 2.2, printed p. 7, to L¹ ∩ L² data and a fixed positive time. See https://arxiv.org/pdf/1407.5289v2 . The Gaussian and gradient bounds of Theorem 1.2 and Corollary 1.2 are separate quantitative inputs, not part of the definition below.

structure OAI.RegularPointCoordinates.IsContinuousHeatKernel line 33
Source documentation
The positive-time representative of the actual Cheeger heat semigroup. The representation is required only for data in L¹ ∩ L². The convolution fields are the Chapman--Kolmogorov identity in the same published Section 2.2; integrability records that its nonnegative integral is finite, rather than relying on the zero convention for undefined integrals.
```
structure IsContinuousHeatKernel (p : ℝ → X → X → ℝ) : Prop where
…
```
def OAI.RegularPointCoordinates.ContinuousHeatKernelInput line 48
Source documentation
Existence of a continuous kernel representing the Cheeger heat semigroup.
```
def ContinuousHeatKernelInput : Prop :=
…
```
theorem OAI.RegularPointCoordinates.exists_cutoff_heat_weight_bound line 57
Source documentation
Compact cutoff makes each positive-time heat weight globally bounded; no uniform Gaussian bound is needed for this existence step.
```
theorem exists_cutoff_heat_weight_bound {t : ℝ} (ht : 0 < t) (x : X) :
    ∃ C : ℝ≥0, ∀ y, ‖χ y * p t x y‖ ≤ C := by
…
```
def OAI.RegularPointCoordinates.cutoffHeatWeightBound line 65
theorem OAI.RegularPointCoordinates.cutoffHeatWeight_le line 68
def OAI.RegularPointCoordinates.cutoffHeatGram line 77
Source documentation
The actual cutoff heat average of the Gram field, with the manuscript's positive scalar regularization. The weight is constructed from the kernel.
```
def cutoffHeatGram {t : ℝ} (ht : 0 < t) (x : X) (lambda : ℝ) : E →L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.cutoffHeatGram_energy line 83
theorem OAI.RegularPointCoordinates.cutoffHeatGram_represents_energy line 92
Source documentation
Whenever a cutoff energy density is represented as an L¹ ∩ L² function, the quadratic form is the actual Cheeger heat semigroup applied to that density, with precisely the added scalar regularization.
```
theorem cutoffHeatGram_represents_energy {t : ℝ} (ht : 0 < t) (lambda : ℝ)
    (v : E) (f : Lp ℝ 2 μ) (hfi : Integrable f μ)
    (hf : f =ᵐ[μ] fun y => χ y * (SobolevSpace.minimalSlope μ hQ (U v) y) ^ 2) :
    (fun x => ⟪v, cutoffHeatGram μ hQ hp hχ hsχ U ht x lambda v⟫_ℝ) =ᵐ[μ]
      fun x => heatAt μ hQ t f x + (lambda * t) * ‖v‖ ^ 2 := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.cutoffHeatGram, OAI.RegularPointCoordinates.heatAt
theorem OAI.RegularPointCoordinates.cutoffHeatGram_isPositive line 108
def OAI.RegularPointCoordinates.cutoffHeatGramEquiv line 117
Source documentation
Strict regularization constructs the inverse of every actual heat Gram operator in finite dimension, at every testing point and positive time.
```
def cutoffHeatGramEquiv [FiniteDimensional ℝ E] (hχpos : ∀ y, 0 ≤ χ y)
    {t : ℝ} (ht : 0 < t) (x : X) {lambda : ℝ} (hlambda : 0 < lambda) : E ≃L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.cutoffHeatGramEquiv_apply line 125