A strong solution is a Leray–Hopf solution #
The translate of a strong solution on [t₀, T] to [0, T - t₀], with an
initial datum that is its almost-everywhere initial slice, satisfies every
clause of the Leray–Hopf definition (prop:lps-local-strong).
theorem
ESS.lps_strong_solution_is_leray_hopf
{t₀ T : ℝ}
{b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{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)
(hb : CKN.IsInJ b)
(hTrace : (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t₀)) =ᵐ[MeasureTheory.volume] b)
:
CKN.IsLerayHopfSolution (T - t₀) b (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => u (z.1, t₀ + z.2))
fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Du (z.1, t₀ + z.2) i
A strong solution on [t₀, T], translated in time to [0, T - t₀], with
datum its almost-everywhere initial slice, is a Leray–Hopf solution
(prop:lps-local-strong).