HeatTimeContinuity.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positive-time continuity derived from the actual heat semigroup

theorem OAI.RegularPointCoordinates.kernelHeat_eq_delayed line 18
Source documentation
Moving time into the L2 heat flow leaves a fixed positive kernel row.
```
theorem kernelHeat_eq_delayed {a t : ℝ} (ha : 0 < a) (hat : a < t)
    (f : Lp ℝ 2 μ) (x : X) :
    kernelHeat μ hQ hk t f x =
      ⟪heatKernelRow μ hQ hk a x, heatAt μ hQ (t - a) f⟫_ℝ := by
…
```
Mentions: OAI.RegularPointCoordinates.kernelHeat, OAI.RegularPointCoordinates.heatKernelRow, OAI.RegularPointCoordinates.heatAt
theorem OAI.RegularPointCoordinates.kernelHeat_continuousOn_time_space line 27
Source documentation
Positive-time continuity requires no extra time-regularity hypothesis on the published kernel representative.
```
theorem kernelHeat_continuousOn_time_space (f : Lp ℝ 2 μ) :
    ContinuousOn (fun tz : ℝ × X => kernelHeat μ hQ hk tz.1 f tz.2) (Ioi 0 ×ˢ univ) := by
…
```
Mentions: OAI.RegularPointCoordinates.kernelHeat
theorem OAI.RegularPointCoordinates.kernel_continuousOn_time_right line 46
Source documentation
The kernel at a fixed first pole is jointly continuous in positive time and its second pole.
```
theorem kernel_continuousOn_time_right (x : X) :
    ContinuousOn (fun tz : ℝ × X => ker tz.1 x tz.2) (Ioi 0 ×ˢ univ) := by
…
```
theorem OAI.RegularPointCoordinates.kernelAverage_continuousOn_time_space line 74
Source documentation
The same joint continuity holds for the actual average kernel.
```
theorem kernelAverage_continuousOn_time_space (A : Set X)
    (hA : MeasurableSet A) (hAt : μ A ≠ ⊤) :
    ContinuousOn (fun tz : ℝ × X => kernelAverage μ ker tz.1 A tz.2) (Ioi 0 ×ˢ univ) := by
…
```
Mentions: OAI.RegularPointCoordinates.kernelAverage