Positive-time Gaussian heat has every actual Sobolev derivative, enabling genuine H∞ approximations.

theorem EulerSobolevHeat.cylinderHeat_all_orders (period : ℝ) [Fact (0 < period)] (q : ℕ) (v : NNReal) (hv : 0 < v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ∃ (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)), EulerCylinderSobolevSpace.value period u = (EulerGaussianCylinderHeat.cylinderHeat period v) f

Positive-time actual cylinder heat belongs to every finite Sobolev space, for every L² datum.

theorem EulerSobolevHeat.mollified_heat_all_memLp (period : ℝ) [Fact (0 < period)] (n : ℕ) (v : NNReal) (hv : 0 < v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (j : ℕ) (w : Fin j → Fin 4) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w (EulerMollifierRepresentative.smoothMollifier period n ((EulerGaussianCylinderHeat.cylinderHeat period v) f))) 2 (EulerLiftedGradientSpace.liftMeasure period)

Mollified positive-time heat has an actual smooth representative whose derivatives of every order are in L².

theorem EulerSobolevHeat.smoothApprox_representative_all (period : ℝ) [Fact (0 < period)] {q : ℕ} (n : ℕ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ∃ (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), ↑↑(EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.smoothApprox period q n) u)) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f ∧ (∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) ∧ ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)

The earlier contractive high-regularity approximations are in fact genuine smooth H∞ fields.