Solenoidal tests in the strong weak equation #
The pressure term in the pressure-inclusive equation vanishes for compactly
supported solenoidal tests (lem:lps-H1-estimate).
theorem
ESS.LPS.lps_strong_solenoidal_weak_equation
{a b : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsLpsStrongSolution a b u Du p)
{φ : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b))
(hdiv :
∀ (z : CKN.Foundation.Parabolic.ParabolicPoint),
∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0)
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3,
∑ j : Fin 3,
u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3,
∑ j : Fin 3, Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z = 0
The pressure-inclusive strong equation reduces to its pressure-free weak
form on every compactly supported solenoidal test field
(lem:lps-H1-estimate).