Leray–Hopf solutions are finite-energy weak solutions with a pressure #
With the canonical associated pressure (thm:assoc-pressure), a Leray–Hopf
solution belongs to the class used by the weak–strong comparison of
lem:pv-serrin-uniqueness. The initial pairing is identified with the datum
through the weak continuity at time zero and the strong L² trace.
theorem
ESS.serrin_integral_mul_tendsto_filter
{ι : Type}
{l : Filter ι}
{f g : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
(hg : MeasureTheory.MemLp g 2 MeasureTheory.volume)
{gseq : ι → CKN.Foundation.Parabolic.Vec3 → ℝ}
(hgseq : ∀ᶠ (n : ι) in l, MeasureTheory.MemLp (gseq n) 2 MeasureTheory.volume)
(herror :
Filter.Tendsto
(fun (n : ι) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => gseq n x - g x) 2 MeasureTheory.volume)
l (nhds 0))
:
Filter.Tendsto (fun (n : ι) => ∫ (x : CKN.Foundation.Parabolic.Vec3), f x * gseq n x) l
(nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), f x * g x))
Pairing against a fixed square-integrable function is continuous along any
filter under L² convergence of the other factor.
theorem
ESS.serrin_trace_filter_neBot
{T : ℝ}
(hT : 0 < T)
:
(nhdsWithin 0 (Set.Ioi 0) ⊓ MeasureTheory.ae (MeasureTheory.volume.restrict (Set.Ioo 0 T))).NeBot
Every right neighborhood of zero meets every full-measure subset of (0, T).
theorem
ESS.lerayHopf_initial_pairing
{T : ℝ}
{a : 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}
(hLH : CKN.IsLerayHopfSolution T a u Du)
{ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψc : HasCompactSupport ψ)
:
The initial pairings of a Leray–Hopf solution with smooth compactly supported fields are those of the datum.
theorem
ESS.serrinWeak_of_lerayHopf
{T : ℝ}
{a : 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}
(hLH : CKN.IsLerayHopfSolution T a u Du)
:
∃ (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ), IsSerrinWeakSolution T a u Du p
A Leray–Hopf solution, with its canonical associated pressure, is a finite-energy weak solution with pressure.