Blowup Riesz Product Test

Pressure reconstruction and convergence bounds for the rescaled sequence.

theorem ESS.blowup_rieszPressureJointLaplacian_product {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {θ : ℝ → ℝ} (hθ : ContDiff ℝ (↑⊤) θ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.Leray.rieszPressureJointLaplacian (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ w.1 * θ w.2) z = θ z.2 * CKN.spatialLaplacian ψ z.1