Heat evolution in the complete Bessel space

The Fourier heat multiplier acts on the weighted L² coordinate of the complete Sobolev carrier, preserving its order and contracting its norm.

noncomputable def CKN.Leray.regularisedBesselHeat (s t : ℝ) (ht : 0 ≤ t) (v : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 s 2) : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 s 2

Heat evolution transported through the Bessel/L² isometry.

Equations

• CKN.Leray.regularisedBesselHeat s t ht v = BesselPotentialSpace.ofLp s (CKN.Leray.heatSemigroup t ht v.toLp)

theorem CKN.Leray.regularisedBesselHeat_norm_le (s t : ℝ) (ht : 0 ≤ t) (v : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 s 2) : ‖regularisedBesselHeat s t ht v‖ ≤ ‖v‖

The heat semigroup contracts every complete Bessel Hˢ norm.

theorem CKN.Leray.regularisedBesselHeat_continuousAt (s : ℝ) {t₀ : ℝ} (ht₀ : 0 ≤ t₀) (v : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 s 2) : ContinuousAt (fun (t : { t : ℝ // 0 ≤ t }) => regularisedBesselHeat s ↑t ⋯ v) ⟨t₀, ht₀⟩

Heat evolution is strongly continuous in the complete Bessel Hˢ space at every nonnegative time, including time zero.

theorem CKN.Leray.regularisedBesselHeat_zero (s : ℝ) (v : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 s 2) : regularisedBesselHeat s 0 ⋯ v = v

Complete Sobolev heat evolution has the prescribed initial value.