Assoc Pressure Vector Potential Decay #
Supporting estimates for the Navier–Stokes development.
noncomputable def
CKN.Leray.associatedPressureVectorTimePartial
(φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3)
:
The componentwise time derivative of a vector test on product space-time coordinates.
Equations
- CKN.Leray.associatedPressureVectorTimePartial φ z i = CKN.timePartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ w i) z
Instances For
def
CKN.Leray.associatedPressureCurlSourceTest
(φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3)
(j : Fin 3)
:
The signed coordinate expression for the curl of a test field in direction j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.Leray.associatedPressureVectorTimePartial_mem_spaceTimeTestFunction
{T : ℝ}
{φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3}
(hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T))
:
The time derivative of a compact space-time test field remains in the same compact test class.
theorem
CKN.Leray.associatedPressureHelmholtzScalarPotential_timePartial
{T : ℝ}
{φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3}
(hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T))
(z : Foundation.Parabolic.Vec3 × ℝ)
:
Time differentiation commutes with the scalar Helmholtz potential.
theorem
CKN.Leray.associatedPressureHelmholtzVectorPotential_component_decay
{T : ℝ}
{φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3}
(hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T))
(j : Fin 3)
:
(RieszPressurePotentialDecay fun (z : Foundation.Parabolic.Vec3 × ℝ) =>
associatedPressureHelmholtzVectorPotential φ z j) ∧ RieszPressurePotentialDecay fun (z : Foundation.Parabolic.Vec3 × ℝ) =>
timePartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureHelmholtzVectorPotential φ w j) z
Each component of the Helmholtz vector potential and its time derivative
has the uniform decay required for spatial cutoff limits in
thm:assoc-pressure.