Heat Critical Space Time #
As the regularization vanishes, the initial regularized entropies converge
to one third of the cubic integral, as used in lem:pv-heat-critical.
theorem
ESS.heatRegEnergy_initial_tendsto_l3
{b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(hb : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i)
(hbc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i)
:
Filter.Tendsto (fun (n : ℕ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy (1 / (↑n + 1)) (b x)) Filter.atTop
(nhds (1 / 3 * ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (b x) ^ 3))
As the regularization vanishes, the initial regularized entropies converge
to one third of the cubic integral, as used in lem:pv-heat-critical.