HeatKernelRows.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Positive-time kernel rows as actual L2 and Sobolev functions

The only kernel input is IsContinuousHeatKernel, including the precise Chapman--Kolmogorov identity of Jiang--Li--Zhang (2016), Section 2.2, printed p. 7. Square integrability, the L2 semigroup evolution and positive-time Sobolev regularity are consequences, rather than extra kernel assumptions.

theorem OAI.RegularPointCoordinates.heatKernel_memLp line 26
def OAI.RegularPointCoordinates.heatKernelRow line 33
Source documentation
The actual L2 kernel row. The value at nonpositive times is unused.
```
def heatKernelRow (t : ℝ) (x : X) : Lp ℝ 2 μ :=
…
```
theorem OAI.RegularPointCoordinates.heatKernelRow_coe line 37
theorem OAI.RegularPointCoordinates.heatKernelRow_inner line 43
theorem OAI.RegularPointCoordinates.heatKernelRow_norm_sq line 57
theorem OAI.RegularPointCoordinates.heatKernelRow_evolves line 64
def OAI.RegularPointCoordinates.heatKernelSobolev line 82
Source documentation
Positive-time kernel rows belong to the actual Cheeger Sobolev space.
```
def heatKernelSobolev (t : ℝ) (ht : 0 < t) (x : X) : SobolevSpace μ hQ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.heatKernelSobolev_toLp line 86
theorem OAI.RegularPointCoordinates.heatKernelSobolev_coe line 95
theorem OAI.RegularPointCoordinates.heatKernelSobolev_weak_laplacian line 101
theorem OAI.RegularPointCoordinates.heatKernelRow_continuous line 108
Source documentation
Spatial continuity in L2, including at every source point.
```
theorem heatKernelRow_continuous {t : ℝ} (ht : 0 < t) :
    Continuous (heatKernelRow μ hQ hp t) := by
…
```
Mentions: OAI.RegularPointCoordinates.heatKernelRow
def OAI.RegularPointCoordinates.kernelHeat line 125
Source documentation
The canonical positive-time continuous representative defined by the kernel.
```
def kernelHeat (t : ℝ) (f : Lp ℝ 2 μ) (x : X) : ℝ :=
…
```
theorem OAI.RegularPointCoordinates.kernelHeat_continuous line 129
theorem OAI.RegularPointCoordinates.kernelHeat_eq_integral line 134
theorem OAI.RegularPointCoordinates.kernelHeat_represents line 143