Strong continuity of the heat evolution

The Gaussian multiplier is strongly continuous on spatial L², including at initial time, as required by lem:reg-local-mild.

noncomputable def CKN.Leray.heatSymbolField (t : ℝ) (F : ↥ComplexVectorL2) : Foundation.Parabolic.L2Vec3 → ComplexVec3

The Fourier-side heat evolution obtained by multiplying a vector field by the heat symbol.

Equations

• CKN.Leray.heatSymbolField t F ξ = CKN.Leray.heatSymbol t ξ • ↑↑F ξ

theorem CKN.Leray.heatMultiplier_smul_continuousAt {t₀ : ℝ} (ht₀ : 0 ≤ t₀) (F : ↥ComplexVectorL2) : ContinuousAt (fun (t : { t : ℝ // 0 ≤ t }) => heatMultiplier ↑t ⋯ • F) ⟨t₀, ht₀⟩

The heat multiplier acting on a fixed frequency-space vector is strongly continuous for nonnegative elapsed times.

theorem CKN.Leray.heatSemigroup_continuousAt {t₀ : ℝ} (ht₀ : 0 ≤ t₀) (F : ↥ComplexVectorL2) : ContinuousAt (fun (t : { t : ℝ // 0 ≤ t }) => heatSemigroup ↑t ⋯ F) ⟨t₀, ht₀⟩

The complex heat semigroup is strongly continuous, including at time zero.

theorem CKN.Leray.realHeatOperator_continuousAt {t₀ : ℝ} (ht₀ : 0 ≤ t₀) (f : ↥RealVectorL2) : ContinuousAt (fun (t : { t : ℝ // 0 ≤ t }) => realHeatOperator ↑t ⋯ f) ⟨t₀, ht₀⟩

The real heat evolution is strongly continuous at every nonnegative time, including the initial state required by lem:reg-local-mild.