Endpoint cross-density limits #
For a Leray--Hopf solution with L²_t L∞_x velocity, both oriented cross
densities have the integrability and cutoff-mollification limits needed for the
cross-testing identity (lem:lps-comparison, endpoint case).
theorem
ESS.lps_component_energy_bound
{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}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsSerrinWeakSolution T a u Du p)
:
∃ (K : ENNReal),
K ≠ ⊤ ∧ ∀ (j : Fin 3),
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, τ) j) 2 MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, τ) j) 2 MeasureTheory.volume ≤ K
A weak solution has uniformly bounded slice L² norms of every velocity
component.
theorem
ESS.lps_mixed_cross_density_limits_endpoint
{T : ℝ}
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{u v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{pu pv : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hULH : CKN.IsLerayHopfSolution T a u Du)
(hVLH : CKN.IsLerayHopfSolution T a v Dv)
(hU : IsSerrinWeakSolution T a u Du pu)
(hV : IsSerrinWeakSolution T a v Dv pv)
(hEndpoint :
∫⁻ (t : ℝ) in Set.Ioo 0 T, essSup
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))))
MeasureTheory.volume ^ 2 < ⊤)
:
(∀ t ∈ Set.Ioo 0 T,
(∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.Integrable (serrinCrossDensity v Dv pv u Du n (serrinCutoff n))
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) ∧ Filter.Tendsto
(fun (n : ℕ) =>
∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), serrinCrossDensity v Dv pv u Du n (serrinCutoff n) q)
Filter.atTop
(nhds
((-∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, u q k * ∑ j : Fin 3, v q j * Dv q k j) - ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du q k j * Dv q k j))) ∧ ∀ t ∈ Set.Ioo 0 T,
(∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.Integrable (serrinCrossDensity u Du pu v Dv n (serrinCutoff n))
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) ∧ Filter.Tendsto
(fun (n : ℕ) =>
∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), serrinCrossDensity u Du pu v Dv n (serrinCutoff n) q)
Filter.atTop
(nhds
((-∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, v q k * ∑ j : Fin 3, u q j * Du q k j) - ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Dv q k j * Du q k j))
Both oriented cross densities have the required integrability and cutoff-mollification limits when the distinguished velocity satisfies the endpoint Serrin condition. The first product is the distinguished velocity against the rival's advective convection.