Top-cylinder Theorem A smallness #
The last step of the uniform interior route to CIV.timeZeroSingularSetNull: from the uniform
interior
Morrey decay of CIV.uniform_morrey_decay_of_top_gradient_small, together with the fixed-scale
Sobolev display and the pointwise-bounded force, the dimensionless Theorem A quantity is small on
a top-boundary cylinder at every interior centre, for a single fixed radius, uniformly in the
base time. The proof applies the fixed-scale display at each interior time on a shrinking window
below the top slice, then passes to the limit along an increasing sequence of base times using
continuity of the Lebesgue integral from below on the resulting monotone family of sets.
A scale small enough for one power-law bound #
Given a nonnegative coefficient, a positive target and a positive exponent, there is a
scale at most 1 making the power-law quantity C * ρ ^ e fall below the target. Used three
times below, once for each of the velocity, pressure and force smallness thresholds.
The volume of the top-boundary cylinder and of the backward cylinder #
The volume of the top-boundary cylinder vec3Ball x ρ ×ˢ Ioo (-(ρ ^ 2)) 0, computed by the
same product-measure display used for the parabolic ball, since the base time interval has the
same length ρ ^ 2 as the backward cylinder's.
The volume of a backward parabolic cylinder in the closed-form display (4π/3) r ^ 5.
The force term is bounded by a pointwise multiple of the cylinder's volume #
On any measurable subset of the unit cylinder where the force is bounded in Euclidean norm
by M, the scale-invariant force integrand is dominated by a constant multiple of the volume of
that subset, with the constant depending only on ρ, q and M.
Splitting the combined integrand into its three terms #
On a fixed measurable set where the velocity and pressure are almost-everywhere strongly measurable, the integral of the combined velocity-cube, pressure and force integrand splits into the sum of the three separate integrals.
Local measurability of the velocity and the pressure #
On a backward cylinder whose closure sits inside the unit cylinder, the velocity is almost everywhere strongly measurable for the restricted volume measure, via the compactly-contained local box the suitable weak-solution class supplies at that closure.
On any subset of the unit cylinder, the pressure is almost everywhere strongly measurable for
the restricted volume measure, directly from the global energy class's L^{3/2} membership.
The force term's radius algebra #
The real-number identity turning the raw force-integral bound (a pointwise bound times the
cylinder's volume) into the same power of ρ used by the force-smallness threshold, times
ρ ^ 2.
The combined bound on one fixed backward cylinder #
At a fixed interior time s and a fixed radius ρ satisfying the uniform Morrey decay of
CIV.uniform_morrey_decay_of_top_gradient_small, the fixed-scale display
CKN.step2_fixed_scale_integrals bounds the velocity and pressure integrals, the pointwise force
bound bounds the force integral, and once ρ is small enough for each of the three
scale-invariant smallness thresholds, their sum over the backward cylinder is at most
ε₀ * ρ ^ 2.
An increasing sequence of base times approaching the top slice #
A strictly increasing sequence of base times inside (-σ, 0), tending to the top slice, whose
associated off-centre cylinders increase to the top-boundary cylinder.
Passing to the top time slice #
If a nonnegative integrand's integral over every off-centre cylinder based at a time in
(-σ, 0) is at most C, then its integral over the top-boundary cylinder is at most C as
well, by continuity of the Lebesgue integral from below along the increasing family of
off-centre cylinders of CIV.exists_increasing_seq_topCylinder.
Monotonicity and the velocity/pressure scale algebra #
The real-number identity turning a bound on the velocity-smallness coefficient
(2 * gagliardoConstant * M₁) ^ 3 * ρ ^ (6/5) into the fixed-scale display's own velocity bound
ρ ^ 2 * (2 * gagliardoConstant * (M₁ * ρ ^ (2/5))) ^ 3, both times ρ ^ 2.
The real-number identity turning a bound on the pressure-smallness coefficient
M₁ ^ (3/2) * ρ ^ (3/5) into the fixed-scale display's own pressure bound
M₁ ^ (3/2) * ρ ^ (13/5), both times ρ ^ 2.
The entrance containment at the top time slice #
An off-centre cylinder based at the top slice 0 and truncated at a base time s ≤ 0 sits
inside the backward parabolic cylinder of the same radius based at s.
Main theorem #
Top-cylinder Theorem A smallness: given the uniform interior Morrey decay constant C₂₇ of
CIV.uniform_morrey_decay_of_top_gradient_small, for every interior centre where the spatial
gradient's top-boundary integral is uniformly small up to a base scale r₀, there is a radius
ρ ≤ r₀ at which the combined velocity, pressure and force integrand of the Theorem A smallness
condition is at most ε₀ * ρ ^ 2 on the top-boundary cylinder based at that centre. The three
smallness thresholds are met by shrinking ρ; the top-boundary integral itself is reached from
the fixed-scale display on backward cylinders by continuity of the Lebesgue integral from below,
along an increasing sequence of base times approaching the top slice.