PlaneHeatTimeContinuity.lean`

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Operator-norm continuity of Gaussian heat operators at every strictly positive time.

def OAI.ForcedComputation.PlaneHeat.timeCore line 14
def OAI.ForcedComputation.PlaneHeat.timeCoefficient line 15
def OAI.ForcedComputation.PlaneHeat.timeEnvelope line 16
def OAI.ForcedComputation.PlaneHeat.timeDerivativeEnvelope line 18
theorem OAI.ForcedComputation.PlaneHeat.oneDim_time_le line 21
theorem OAI.ForcedComputation.PlaneHeat.kernel_time_le line 38
theorem OAI.ForcedComputation.PlaneHeat.derivative_time_le line 48
theorem OAI.ForcedComputation.PlaneHeat.timeCore_integrable line 57
theorem OAI.ForcedComputation.PlaneHeat.timeMoment_integrable line 60
theorem OAI.ForcedComputation.PlaneHeat.product_integrable line 65
theorem OAI.ForcedComputation.PlaneHeat.timeEnvelope_integrable line 69
theorem OAI.ForcedComputation.PlaneHeat.timeDerivativeEnvelope_integrable line 74
theorem OAI.ForcedComputation.PlaneHeat.oneDim_time_continuousAt line 92
theorem OAI.ForcedComputation.PlaneHeat.kernel_time_continuousAt line 97
theorem OAI.ForcedComputation.PlaneHeat.derivative_time_continuousAt line 101
theorem OAI.ForcedComputation.PlaneHeat.kernel_l1_tendsto line 111
Source documentation
Gaussian kernels are continuous in L1 at every strictly positive time.
```
theorem kernel_l1_tendsto {t : ℝ} (ht : 0 < t) :
    Tendsto (fun s => ∫ y, |kernel s y - kernel t y|) (𝓝 t) (𝓝 0) := by
…
```
Mentions: OAI.ForcedComputation.PlaneHeat.kernel
theorem OAI.ForcedComputation.PlaneHeat.kernelDerivative_l1_tendsto line 141
Source documentation
The Cartesian Gaussian derivatives are also continuous in L1 at positive time.
```
theorem kernelDerivative_l1_tendsto {t : ℝ} (ht : 0 < t) (j : Fin 2) :
    Tendsto (fun s => ∫ y, |kernelDerivative s j y - kernelDerivative t j y|) (𝓝 t) (𝓝 0) := by
…
```
Mentions: OAI.ForcedComputation.PlaneHeat.kernelDerivative
theorem OAI.ForcedComputation.PlaneHeat.continuous_heatOperator line 173
Source documentation
Heat operators depend continuously on positive time in the operator norm on C_b^k.
```
theorem continuous_heatOperator (k : ℕ) :
    Continuous (fun t : {t : ℝ // 0 < t} => heatOperator F k t.val t.property) := by
…
```
Mentions: OAI.ForcedComputation.PlaneHeat.heatOperator
theorem OAI.ForcedComputation.PlaneHeat.continuous_gradientOperator line 183
Source documentation
The singular gradient bound causes no loss of operator continuity away from time zero.
```
theorem continuous_gradientOperator (k : ℕ) (j : Fin 2) :
    Continuous (fun t : {t : ℝ // 0 < t} => gradientOperator F k t.val t.property j) := by
…
```
Mentions: OAI.ForcedComputation.PlaneHeat.gradientOperator