The leading pressure term away from the cut-off

The leading local pressure p₁ = ηp - (p₂ + ⋯ + p₈) is built from ηp and from Newtonian potentials whose sources all vanish outside tsupport η. Consequently p₁ is harmonic in the sense of distributions outside tsupport η: a test function vanishing on an open neighbourhood of the cut-off support pairs to zero against Δp₁. This is the exterior half of the whole-space distributional identity for p₁; the interior half is the localized identity of the pressure decomposition.

theorem CKN.pressureCutoff_spatialDeriv_eqOn_zero {ψ : Foundation.Parabolic.Vec3 → ℝ} {V : Set Foundation.Parabolic.Vec3} (hV : IsOpen V) (hψV : Set.EqOn ψ (fun (x : Foundation.Parabolic.Vec3) => 0) V) (i : Fin 3) : Set.EqOn (spatialDeriv ψ i) (fun (x : Foundation.Parabolic.Vec3) => 0) V

A smooth function vanishing on an open set has vanishing first spatial derivatives there.

theorem CKN.pressureCutoff_mixedSecond_eqOn_zero {ψ : Foundation.Parabolic.Vec3 → ℝ} {V : Set Foundation.Parabolic.Vec3} (hV : IsOpen V) (hψV : Set.EqOn ψ (fun (x : Foundation.Parabolic.Vec3) => 0) V) (i j : Fin 3) : Set.EqOn (mixedSecond ψ i j) (fun (x : Foundation.Parabolic.Vec3) => 0) V

A smooth function vanishing on an open set has vanishing mixed second spatial derivatives there.

theorem CKN.pressureCutoff_spatialLaplacian_eqOn_zero {ψ : Foundation.Parabolic.Vec3 → ℝ} {V : Set Foundation.Parabolic.Vec3} (hV : IsOpen V) (hψV : Set.EqOn ψ (fun (x : Foundation.Parabolic.Vec3) => 0) V) : Set.EqOn (spatialLaplacian ψ) (fun (x : Foundation.Parabolic.Vec3) => 0) V

A smooth function vanishing on an open set has vanishing spatial Laplacian there.

theorem CKN.pressureP1_slice_locallyIntegrable {η : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → 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) (hp : MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => p (y, s)) (tsupport η) MeasureTheory.volume) (hf : ∀ (j : Fin 3), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => f (y, s) j) (tsupport η) MeasureTheory.volume) : MeasureTheory.LocallyIntegrable (pressureP1 η u c p f s) MeasureTheory.volume

The leading local pressure is locally integrable on every time slice for which the velocity tensor, the pressure and the force are integrable on the cut-off support.

theorem CKN.pressureCutoff_tensorPairing_eq_zero_of_eqOn_zero {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {s : ℝ} {ψ : Foundation.Parabolic.Vec3 → ℝ} {V : Set Foundation.Parabolic.Vec3} (hV : IsOpen V) (hηV : tsupport η ⊆ V) (hψV : Set.EqOn ψ (fun (x : Foundation.Parabolic.Vec3) => 0) V) : ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, η x * pressureUTensor u c (x, s) i j * mixedSecond ψ i j x = 0

The tensor side of the whole-space identity vanishes against a test function supported away from the cut-off.

theorem CKN.pressureP1_pairing_eq_zero_of_eqOn_zero {η : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → 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) (hp : MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => p (y, s)) (tsupport η) MeasureTheory.volume) (hf : ∀ (j : Fin 3), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => f (y, s) j) (tsupport η) MeasureTheory.volume) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) {V : Set Foundation.Parabolic.Vec3} (hV : IsOpen V) (hηV : tsupport η ⊆ V) (hψV : Set.EqOn ψ (fun (x : Foundation.Parabolic.Vec3) => 0) V) : ∫ (x : Foundation.Parabolic.Vec3), pressureP1 η u c p f s x * spatialLaplacian ψ x = 0

The leading local pressure is weakly harmonic outside the support of the cut-off: a smooth compactly supported test function vanishing on an open neighbourhood of tsupport η pairs to zero against Δp₁.