Eventual equality for Helmholtz cutoffs #
Cutoff derivatives agree pointwise with the uncut Helmholtz decomposition.
theorem
CKN.Leray.associatedPressureHelmholtzTestCutoff_spatial_eventually_eq
{T : ℝ}
{φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3}
(hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T))
(i j : Fin 3)
(z : Foundation.Parabolic.Vec3 × ℝ)
:
∀ᶠ (n : ℕ) in Filter.atTop, spatialPartialProd (fun (q : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureHelmholtzTestCutoff φ n q i) j z = spatialPartialProd (fun (q : Foundation.Parabolic.Vec3 × ℝ) => φ q i) j z
Spatial derivatives of the Helmholtz cutoffs eventually equal those of
the original test, as used in thm:assoc-pressure.
theorem
CKN.Leray.associatedPressureHelmholtzTestCutoff_time_eventually_eq
{T : ℝ}
{φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3}
(hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T))
(i : Fin 3)
(z : Foundation.Parabolic.Vec3 × ℝ)
:
∀ᶠ (n : ℕ) in Filter.atTop, timePartialProd (fun (q : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureHelmholtzTestCutoff φ n q i) z = timePartialProd (fun (q : Foundation.Parabolic.Vec3 × ℝ) => φ q i) z
Time derivatives of the Helmholtz cutoffs eventually equal those of the
original test, as used in thm:assoc-pressure.