KernelRowL2.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RegularPointCoordinates.heatKernelRow_memLp line 20
Source documentation
The kernel convolution identity itself gives square integrability.
```
theorem heatKernelRow_memLp (s : ℝ) (hs : 0 < s) (y : X) : MemLp (ker s y) 2 μ := by
…
```
def OAI.RegularPointCoordinates.heatKernelRowLp line 28
Source documentation
A positive-time kernel row as an actual L² function.
```
def heatKernelRowLp (s : ℝ) (hs : 0 < s) (y : X) : Lp ℝ 2 μ :=
…
```
theorem OAI.RegularPointCoordinates.heatKernelRowLp_coe line 31
theorem OAI.RegularPointCoordinates.heatAt_kernelRow line 35
Source documentation
The abstract L² heat evolution agrees with the next kernel row.
```
theorem heatAt_kernelRow (s T : ℝ) (hs : 0 < s) (hT : 0 < T) (y : X) :
    heatAt μ hQ T (heatKernelRowLp μ hQ hk s hs y) =ᵐ[μ]
      fun x => ker (T+s) x y := by
…
```
Mentions: OAI.RegularPointCoordinates.heatAt, OAI.RegularPointCoordinates.heatKernelRowLp