The pressure-gradient boundary from a cell estimate on the origin cell #
prop:bootstrap is proved by a finite spatial cover, a slice-wise estimate,
and a passage through Fubini, all of which produce a bound on every Morrey
cell of the gradient rather than on the Morrey seminorm directly. The
seminorm is the supremum of those cells, so the two forms differ only by one
supremum.
This module records that last step: from a cell estimate carried by the
one-sided cylinder parabolicCylinder 0 0 R₁, with the three regularity
conjuncts of the selected gradient field, the explicit-majorant statement
oneSidedPressureGradientQuantitative follows, and with it the existential
form the small-data statement consumes. The hypothesis is stated with the
same numerical binders, the same domain hypothesis
closure (parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I, and the same
majorant formula as its conclusion, so nothing is strengthened on the way.
The last four theorems record why the carrier of that hypothesis has to be
the one-sided cylinder. A symmetric parabolic ball around a point always
contains times strictly after that point, and the closed backward cylinder
around the same point contains none. Since the closed unit backward cylinder
is itself a space-time product set, the domain hypothesis of thm:A does not
imply the corresponding inclusion for any symmetric ball about the origin.
The explicit-majorant form of prop:bootstrap from a cell estimate on the
origin cell. Only the Morrey supremum is taken here; the three regularity
conjuncts of the selected gradient field pass through unchanged.
The existential form consumed by thm:A, from the same cell estimate.
Display eq:parabolic-ball: the point advanced in time by half the
squared radius lies in the symmetric parabolic ball of that radius.
A consequence of the cylinder definition eq:cylinder: its closure at a
positive radius is the space-time product of a closed spatial ball with a
closed time interval.
A symmetric parabolic ball is never contained in the closed backward cylinder about its own centre, at any pair of positive radii.
The domain hypothesis of thm:A does not imply the same inclusion for a
symmetric parabolic ball about the origin: the closed unit backward cylinder
is itself an admissible space-time set, and no symmetric ball fits inside it.
This is why the cell estimate consumed above carries its own domain
hypothesis on the one-sided cylinder.