The rescaled whole-space pressure is the pressure of the rescaled tensor

The rescaled fixed pressure p₁^k of prop:blowup-limit equals the whole-space Riesz pressure of the rescaled velocity tensor v^k ⊗ v^k (lem:pressure-split). On almost every time slice both solve the same Poisson equation in all of space and lie in L^(3/2), so their difference is a harmonic L^(3/2) function and vanishes by the Liouville theorem.

theorem ESS.blowupLimitAssemblyPressure_ae_eq_of_slices {A B : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hA : MeasureTheory.AEStronglyMeasurable A MeasureTheory.volume) (hB : Measurable B) (h : ∀ᵐ (t : ℝ), (fun (x : CKN.Foundation.Parabolic.Vec3) => A (x, t)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => B (x, t)) : A =ᵐ[MeasureTheory.volume] B

Slicewise almost-everywhere equality of a strongly measurable and a measurable scalar space-time field gives space-time almost-everywhere equality.

theorem ESS.blowupLimitAssemblyPressure_memLp_comp_affine {g : CKN.Foundation.Parabolic.Vec3 → ℝ} {p : ENNReal} (hg : MeasureTheory.MemLp g p MeasureTheory.volume) (x₀ : CKN.Foundation.Parabolic.Vec3) {r : ℝ} (hr : 0 < r) : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x₀ + r • x)) p MeasureTheory.volume

An L^p function composed with a positive spatial dilation and translation stays in L^p.

theorem ESS.blowupLimitAssemblyPressure_integrable_mul_laplacian {h : CKN.Foundation.Parabolic.Vec3 → ℝ} (hh : MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => h x * CKN.spatialLaplacian ψ x) MeasureTheory.volume

A scalar field in L^(3/2) of space pairs integrably with the Laplacian of a compactly supported smooth test.

theorem ESS.blowupLimitAssemblyPressure_poisson_unique {A B : CKN.Foundation.Parabolic.Vec3 → ℝ} {F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (hA : MeasureTheory.MemLp A (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hB : MeasureTheory.MemLp B (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hAeq : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : CKN.Foundation.Parabolic.Vec3), A x * -CKN.spatialLaplacian ψ x = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), F i j x * CKN.mixedSecond ψ i j x) (hBeq : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : CKN.Foundation.Parabolic.Vec3), B x * -CKN.spatialLaplacian ψ x = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), F i j x * CKN.mixedSecond ψ i j x) : A =ᵐ[MeasureTheory.volume] B

Two L^(3/2) solutions of the same whole-space pressure Poisson equation agree almost everywhere.

theorem ESS.blowupLimitAssemblyPressure_riesz_rescale (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (CKN.pressureSplitTensor u i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hp₁ : MeasureTheory.AEStronglyMeasurable (pressureSplitRieszPressure (CKN.pressureSplitTensor u) hF) (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo (-1) 0))) (Mₚ : ENNReal) (hMₚ : Mₚ < ⊤) (hsourceP : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => pressureSplitRieszPressure (CKN.pressureSplitTensor u) hF (x, s)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => pressureSplitRieszPressure (CKN.pressureSplitTensor u) hF (x, s)) (3 / 2) MeasureTheory.volume ≤ Mₚ) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (hv : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => blowupVelocity x₀ t₀ r u z i * blowupVelocity x₀ t₀ r u z j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) : (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => blowupRieszPressure x₀ t₀ r (pressureSplitRieszPressure (CKN.pressureSplitTensor u) hF) z) =ᵐ[MeasureTheory.volume] CKN.Leray.rieszPressureSpaceTime (3 / 2) blowupLimitAssemblyPressure_riesz_rescale._proof_1 (fun (i j : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => blowupVelocity x₀ t₀ r u z i * blowupVelocity x₀ t₀ r u z j) hv

The rescaled fixed whole-space pressure is, almost everywhere, the whole-space Riesz pressure of the tensor of the rescaled zero-extended velocity (lem:pressure-split, used in prop:blowup-limit).