Assoc Pressure Solenoidal Cutoff

Supporting estimates for the Navier–Stokes development.

noncomputable def CKN.Leray.associatedPressureHelmholtzCutoffVectorPotential (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (n : ℕ) : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3

The spatially cut off vector potential used to test the Leray--Hopf equation in the proof of lem:helmholtz-test.

Equations

• CKN.Leray.associatedPressureHelmholtzCutoffVectorPotential φ n z = CKN.Leray.rieszPressurePotentialCutoff n z.1 • CKN.Leray.associatedPressureHelmholtzVectorPotential φ z

theorem CKN.Leray.associatedPressureHelmholtzCutoffVectorPotential_mem_spaceTimeTestFunction {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (n : ℕ) : associatedPressureHelmholtzCutoffVectorPotential φ n ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)

The vector-potential cutoff belongs to the compact test class on the original time slab.

theorem CKN.Leray.associatedPressureHelmholtzCutoffCurl_mem_spaceTimeTestFunction {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (n : ℕ) : associatedPressureTestCurl (associatedPressureHelmholtzCutoffVectorPotential φ n) ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)

The curl of the cut off vector potential is a solenoidal test in the Leray--Hopf equation.

theorem CKN.Leray.associatedPressureHelmholtzCutoffCurl_momentum_zero {T : ℝ} {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} (hLH : IsLerayHopfSolution T a u Du) {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (n : ℕ) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), -∑ i : Fin 3, u z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => associatedPressureTestCurl (associatedPressureHelmholtzCutoffVectorPotential φ n) (Foundation.Parabolic.parabolicHomeomorph y) i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => associatedPressureTestCurl (associatedPressureHelmholtzCutoffVectorPotential φ n) (Foundation.Parabolic.parabolicHomeomorph y) i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => associatedPressureTestCurl (associatedPressureHelmholtzCutoffVectorPotential φ n) (Foundation.Parabolic.parabolicHomeomorph y) i) j z = 0

The solenoidal cutoff tests give zero in the Leray--Hopf momentum identity.