ε-regularity at the blow-up time #
The manuscript applies an ε-regularity criterion at points (x, 0) of the top boundary of
Q = B(1) × (-1, 0), where the solution is not defined; the criterion available here,
CKN.epsilonRegularityL3, is an interior statement on an open space-time set and is therefore
used only at interior base points (x, t) with t < 0, at the fixed scale r / 2. Its
conclusion is quantitative and scale invariant, so the resulting bound does not depend on t,
and a countable family of the resulting half cylinders covers B(x₀, r/2) × (-r²/4, 0). This is
the route to eq:interior:regular described in design note R3.
The dimensionless smallness quantity on a cylinder of radius μ is
μ⁻² ∫ |u|³ + μ⁻² ∫ |π|^{3/2} + μ^{3q-5} ∫ |f|^q: the velocity and pressure terms carry the same
power of μ and the force term does not, because u, π and f rescale by μ, μ² and μ³
while the cylinder has measure μ⁵. The hypothesis below is the single integral
∫ (|u|³ + |π|^{3/2} + μ^{3q-3} |f|^q) ≤ ε₀ μ², which is exactly that quantity multiplied by
μ², and exactly the hypothesis of CKN.epsilonRegularityL3 for the rescaled fields.
A real power of a product of nonnegative reals, read in ℝ≥0∞.
The integrand of the smallness hypothesis of CKN.epsilonRegularityL3 for the fields
rescaled by μ at z₀ equals μ³ times the integrand of the smallness hypothesis at scale μ,
evaluated at the rescaled point. The three powers μ, μ², μ³ of CKN.rescaleVelocity,
CKN.rescalePressure and CKN.rescaleForce contribute μ³, μ³ and μ^{3q}, and the factor
μ^{3q-3} on the force term is what makes the three contributions share the factor μ³.
ε-regularity at an interior base point, rescaled to an arbitrary radius: there are
universal ε₀ > 0 and C ≥ 0, depending only on the force exponent q, such that if the
closed cylinder B(x₀, μ) × [t₀ - μ², t₀] lies in the domain and the dimensionless quantity
μ⁻² ∫ (|u|³ + |π|^{3/2}) + μ^{3q-5} ∫ |f|^q over B(x₀, μ) × (t₀ - μ², t₀] is at most ε₀,
then |u| ≤ C / μ almost everywhere on B(x₀, μ/2) × (t₀ - μ²/4, t₀]. This is
CKN.epsilonRegularityL3 transported by CKN.isSuitableWeakSolutionIntegrable_rescale, with
the conversions isSuitableWeakSolutionIntegrable_of_isSuitableWeakSolution and
isSuitableWeakSolution_of_integrable between the two suitable-solution predicates; the
constants are
the ε₀ and C₄ of that theorem.
ε-regularity at a point of the blow-up time: if the dimensionless L³ quantity of
CKN.epsilonRegularityL3 is small on the backward cylinder B(x₀, r) × (-r², 0), then u is
bounded by K / r almost everywhere on B(x₀, r/2) × (-r²/4, 0), for universal ε₀ > 0 and
K ≥ 0 depending only on the force exponent q. The solution need not be defined at the top
time t = 0: the bound is obtained from ae_norm_le_of_small_L3_cylinder at the interior base
points (x, t) with t < 0 at the single scale r / 2, and a countable family of the resulting
half cylinders covers B(x₀, r/2) × (-r²/4, 0). Design note R3.
bounded_of_small_L3_top with the two parts of the smallness hypothesis separated, each
with its own power of r: ∫ (|u|³ + |π|^{3/2}) ≤ ε₀ r² on the backward cylinder, and
∫ |f|^q ≤ ε₀ r^{5-3q}. Splitting the single integral of bounded_of_small_L3_top uses
additivity of the lower Lebesgue integral, which is why the measurability of the velocity and of
the pressure on the cylinder is a hypothesis here; the solution class supplies it on every box
compactly contained in the domain.
The everywhere form of bounded_of_small_L3_top for a continuous representative: on the
open set B(x₀, r/2) × (-r²/4, 0) an almost-everywhere bound on a continuous function is a bound
at every point, because a nonempty open subset has positive measure. This is the form in which
eq:interior:regular is used.