The translated solenoidal weak equation

A strong solution on [t₀, T], translated in time to [0, T - t₀], satisfies the pressure-free weak momentum equation against solenoidal tests (prop:lps-local-strong).

theorem ESS.LPS.lps_shift_momentum {t₀ T : ℝ} {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 t₀ T u Du p) (φ : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 (T - t₀)) → (∀ (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 0 (T - t₀)), -∑ i : Fin 3, u (lpsShift t₀ z) i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u (lpsShift t₀ z) i * u (lpsShift t₀ z) j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du (lpsShift t₀ z) i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z = 0

The translated strong solution satisfies the weak momentum equation against every smooth compactly supported solenoidal test field.