The whole-space distributional identity for the leading pressure term

The localized identity for p₁ tests against spatial test functions supported in the solution domain. Splitting an arbitrary compactly supported smooth test function ψ with an auxiliary cut-off χ that equals one on a neighbourhood of tsupport η and is supported in the domain writes ψ = χψ + (1 - χ)ψ: the first piece is admissible for the localized identity, and the second piece vanishes on a neighbourhood of tsupport η, so both sides of the identity vanish on it. The result is the identity tested against every compactly supported smooth ψ, which is the form the Liouville identification consumes.

theorem CKN.exists_cutoff_eqOn_one_of_isCompact {K U : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ (χ : Foundation.Parabolic.Vec3 → ℝ) (V : Set Foundation.Parabolic.Vec3), ContDiff ℝ (↑⊤) χ ∧ HasCompactSupport χ ∧ tsupport χ ⊆ U ∧ IsOpen V ∧ K ⊆ V ∧ Set.EqOn χ (fun (x : Foundation.Parabolic.Vec3) => 1) V

A compact set inside an open set carries a smooth compactly supported cut-off that is identically one on an open neighbourhood of the compact set and is supported in the open set.

theorem CKN.spatialDeriv_add_smooth {F G : Foundation.Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (i : Fin 3) : spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => F y + G y) i = fun (x : Foundation.Parabolic.Vec3) => spatialDeriv F i x + spatialDeriv G i x

Additivity of the first spatial derivative on smooth functions.

theorem CKN.mixedSecond_add_smooth {F G : Foundation.Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (i j : Fin 3) (x : Foundation.Parabolic.Vec3) : mixedSecond (fun (y : Foundation.Parabolic.Vec3) => F y + G y) i j x = mixedSecond F i j x + mixedSecond G i j x

Additivity of the mixed second spatial derivative on smooth functions.

theorem CKN.spatialLaplacian_add_smooth {F G : Foundation.Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (x : Foundation.Parabolic.Vec3) : spatialLaplacian (fun (y : Foundation.Parabolic.Vec3) => F y + G y) x = spatialLaplacian F x + spatialLaplacian G x

Additivity of the spatial Laplacian on smooth functions.

theorem CKN.pressureCutoff_tensorPairing_integrable {η : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {s : ℝ} (hU : ∀ (i j : Fin 3), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j) (tsupport η) MeasureTheory.volume) {φ : Foundation.Parabolic.Vec3 → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, η x * pressureUTensor u c (x, s) i j * mixedSecond φ i j x) MeasureTheory.volume

The tensor pairing integrand is integrable on each admissible time slice.

theorem CKN.pressureP1_wholeSpace_pairing_ae_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {η : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηΩ : tsupport η ⊆ Ω) (c : ℝ → Foundation.Parabolic.Vec3) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∫ (x : Foundation.Parabolic.Vec3), pressureP1 η u c p f s x * spatialLaplacian ψ x = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, η x * pressureUTensor u c (x, s) i j * mixedSecond ψ i j x

The whole-space distributional identity for the leading local pressure. For almost every time the pairing of p₁(·, s) against Δψ equals the tensor pairing of η U(·, s) against the Hessian of ψ, now for an arbitrary smooth compactly supported spatial test function ψ, with no support restriction.