Blowup Riesz Time Slice

Pressure reconstruction and convergence bounds for the rescaled sequence.

theorem ESS.blowup_rieszPressure_exterior_product_pairing_zero (F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (U : Set CKN.Foundation.Parabolic.Vec3) (hzero : ∀ (i j : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ), z.1 ∈ U → F i j z = 0) {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ U) {θ : ℝ → ℝ} (hθ : ContDiff ℝ (↑⊤) θ) (hθc : HasCompactSupport θ) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressure_exterior_product_pairing_zero._proof_1 F hF z * (θ z.2 * CKN.spatialLaplacian ψ z.1) = 0

Exterior-supported tensors give a zero space-time Laplacian pairing for separated spatial and temporal tests.

theorem ESS.blowup_pressure_mul_product_laplacian_integrable {p : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) {θ : ℝ → ℝ} (hθ : ContDiff ℝ (↑⊤) θ) (hθc : HasCompactSupport θ) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z * (θ z.2 * CKN.spatialLaplacian ψ z.1)) MeasureTheory.volume

The product of an L^(3/2) pressure and a separated smooth compact test with a spatial Laplacian is integrable on space-time.

theorem ESS.blowup_pressure_product_laplacian_fubini {p : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) {θ : ℝ → ℝ} (hθ : ContDiff ℝ (↑⊤) θ) (hθc : HasCompactSupport θ) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), p z * (θ z.2 * CKN.spatialLaplacian ψ z.1) = ∫ (t : ℝ), θ t * ∫ (x : CKN.Foundation.Parabolic.Vec3), p (x, t) * CKN.spatialLaplacian ψ x

Fubini separates the time weight from a pressure Laplacian pairing.

theorem ESS.blowup_pressure_slice_laplacian_locallyIntegrable {p : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) {a b : ℝ} (hab : a < b) : MeasureTheory.LocallyIntegrableOn (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), p (x, t) * CKN.spatialLaplacian ψ x) (Set.Ioo a b) MeasureTheory.volume

A global L^(3/2) pressure has a locally integrable time function of its pairings with any compact spatial Laplacian test.

theorem ESS.blowup_rieszPressure_exterior_slice_pairing_ae (F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (U : Set CKN.Foundation.Parabolic.Vec3) (hzero : ∀ (i j : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ), z.1 ∈ U → F i j z = 0) {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ U) {a b : ℝ} (hab : a < b) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressure_exterior_product_pairing_zero._proof_1 F hF (x, t) * CKN.spatialLaplacian ψ x = 0

For each fixed spatial test, the pressure of an exterior tensor has zero spatial Laplacian pairing on almost every time slice.