The velocity is locally L^{10/3}, hence locally L³ #
The data clauses of def:sws place the velocity in L^∞_t L²_x ∩ L²_t H¹_x on
every local box. Two of the terms of the local energy inequality - the cubic
term |u|² u · ∇ψ and the pressure term p u · ∇ψ - are not integrable for a
field that is merely square integrable, so those two terms need the parabolic
interpolation
L^∞_t L²_x ∩ L²_t homogeneous H¹_x ↪ L^{10/3}_{t,x},
which is the content of CKN.ball_time_sobolev. This file turns that estimate
into the three local statements the energy inequality actually consumes: the
velocity is cubed-integrable, the pressure times the velocity is integrable, and
the force times the velocity is integrable, all on an arbitrary compact subset of
the space-time carrier.
Two features of the interpolation shape the file.
- It lives on Euclidean balls, because the spatial factor of a local box is an
arbitrary open set and carries no Sobolev extension. The reduction to balls is
CKN.exists_localBox_ball_cover_of_data; the time factor of the box is used unchanged, since the interpolation accepts any order-connected time set. - Its hypothesis on spatial slices asks for a genuine
CKN.H1Functionon the ball for almost every time. The data clauses give an almost-everywhere weak gradient on the box and, after a slicing argument for the joint energy, an almost-everywhere square-integrable slice; those two are assembled here into the required slice representative and restricted to the ball.
Everything below takes CKN.IsSuitableWeakSolutionData, never the full class, so
these lemmas may be used while the integrability clauses of def:sws are still
being established.
The sup norm ‖·‖ of Vec3 is the one the data clauses use, while the energy
density of the paper is the Euclidean norm CKN.Foundation.Parabolic.vec3EuclideanNorm.
Both comparisons needed here are the easy direction of the equivalence of the two
norms: a component is bounded by the sup norm on the way into the interpolation,
and the Euclidean norm is bounded by √3 times the sup norm on the way out.
Exponents #
The data clauses record the pressure exponent as ENNReal.ofReal (3 / 2) and the
interpolation records its own exponent as ENNReal.ofReal (10 / 3), while the
Hölder machinery of Mathlib is stated for extended-real numerals. The two
bridges below and the Hölder pairing 3 / 2 with 3 are what connect them;
Mathlib supplies no such pairing for these numerals.
The pressure exponent of def:sws as an extended-real numeral.
The velocity exponent used below as an extended-real numeral.
Hölder's inequality pairs L^{3/2} with L³ to give L¹, because
2 / 3 + 1 / 3 = 1. This is the pairing behind both the pressure term and the
force term of the local energy inequality.
L^p membership through the Lebesgue integral #
The data clauses state their finiteness with Lebesgue integrals of powers of the
extended norm, whereas the interpolation and Hölder's inequality both speak of
MeasureTheory.MemLp. The two are the same statement for a finite exponent, and
the translations are collected here once.
Spatial slices of the velocity #
The interpolation is proved slice by slice in time, so it asks for a spatial Sobolev representative at almost every time. The data clauses give the joint finiteness of the energy on the box and an almost-everywhere weak gradient on the box; the first is turned into almost-everywhere square integrability of the slices by the product structure of Lebesgue measure on space-time, and the two are then combined.
The interpolation on one ball cylinder #
Each velocity component is L^{10/3} on a cylinder whose spatial factor is a
ball inside the spatial factor of a local box and whose time factor is the time
factor of that box. This is CKN.ball_time_sobolev applied componentwise; the
hypothesis that a component is square integrable costs nothing, because a
component is bounded by the supremum norm the data clauses control.
Cubic integrability on a compact set #
The velocity is L³ on every compact subset of the space-time carrier. The
compact set is covered by finitely many ball cylinders of one local box, each
cylinder carries the L^{10/3} bound of the interpolation, and each cylinder has
finite measure, so the exponent drops from 10 / 3 to 3 there; the finitely
many bounds are then added.
The cube of the Euclidean norm of the velocity, which is the density of the cubic term of the local energy inequality, is integrable on every compact subset of the space-time carrier.
The two Hölder pairings against the velocity #
The pressure times a velocity component is integrable on every compact subset
of the space-time carrier: the pressure is L^{3/2} by the data clauses and the
velocity is L³ by the interpolation.
A force component times a velocity component is integrable on every compact
subset of the space-time carrier. The force exponent of def:sws exceeds
5 / 2, hence exceeds 3 / 2, and the compact set has finite measure, so the
same 3 / 2 with 3 pairing applies.