The L⁶ bound and the closure of lem:aniso:closure #
This file assembles the last two steps of the closure argument lem:aniso:closure of
Regularity of asymptotically axisymmetric solutions to the 3D Navier–Stokes equations with
analytic forcing, arXiv:2609.20803.
The first step turns the weighted enstrophy bound Y t + 1 ≤ C' (-t)^(-C_* η) of
closure_gronwall_bound into a spatial L⁶ bound on a fixed ball,
‖u(·,t)‖_{L⁶(B(ρ))} ≤ C'' (-t)^(-C_* η / 2) for t ∈ (t_η, 0).
It combines three ingredients: the elliptic gradient bound
integral_sq_fderiv_smul_le, which controls ∫ |∇(χ u)|² by 2 Y + C; the Sobolev
inequality exists_sobolev_six_const, consumed through lintegral_pow_six_le_of_eq_on_ball;
and the enstrophy bound itself.
The Sobolev step is scalar, while the target is the Euclidean norm vec3EuclideanNorm of a
vector field. The bridge is lintegral_pow_six_euclideanNorm_le_sum_components: the Euclidean
norm is dominated pointwise by the ℓ¹ norm of the components
(vec3EuclideanNorm_le_sum_abs), and the L⁶ triangle inequality then splits the ball
integral into the three componentwise ones that the scalar lemma bounds.
A second mismatch is the norm on Vec3 = Fin 3 → ℝ, which is the sup norm. The Sobolev
inequality is phrased with the operator norm ‖fderiv ℝ g x‖ of the differential, whereas the
elliptic bound produces the coordinate sum ∑ⱼ (∂ⱼ g)². Since the dual of the sup norm is the
ℓ¹ norm, sq_opNorm_le_three_mul_sum_sq_basisVec gives ‖fderiv ℝ g x‖² ≤ 3 ∑ⱼ (∂ⱼ g x)²,
which is what eLpNorm_fderiv_comp_two_le integrates.
The second step specialises η = 1 / (16 C_*), so that the L⁶ decay exponent is
β = C_* η / 2 = 1/32 and 4β = 1/8 < 1. That is exactly the range in which
gkt_smallness_of_l6_bound converts the L⁶ bound into the parabolic smallness hypothesis of
the Gustafson–Kang–Tsai criterion, which is the conclusion closure_from_enstrophy_bound.
Two pointwise comparisons on Vec3 #
The Euclidean norm of a vector in Vec3 is at most the sum of the absolute values of its
components.
Vec3 carries the sup norm, so the dual norm of a linear functional is its ℓ¹ norm in the
coordinate basis. Comparing ℓ¹ with ℓ² in three coordinates gives
‖L‖² ≤ 3 ∑ⱼ (L eⱼ)².
The scalar-to-vector bridge on a ball #
The bridge between the scalar L⁶ estimate lintegral_pow_six_le_of_eq_on_ball and the
vector-valued target: on a ball the L⁶ norm of the Euclidean length of v is at most the sum
of the L⁶ norms of its three components. Only a continuous representative w agreeing with
v on the ball is required, which is how the estimate is used: w = χ • u(·,t) is globally
smooth while u(·,t) is smooth only on an open set.
From the coordinate gradient energy to the Sobolev right-hand side #
The L² norm of the differential of one component of a smooth compactly supported field,
in terms of the coordinate gradient energy that the elliptic bound controls.
The L⁶ bound on a ball from a gradient-energy bound #
The L⁶ norm of v on a ball, bounded by the gradient energy of a smooth compactly
supported field w that agrees with v on that ball. This packages the Sobolev inequality
(through lintegral_pow_six_le_of_eq_on_ball), the scalar-to-vector bridge, and the
sup-norm/coordinate comparison of eLpNorm_fderiv_comp_two_le.
The L⁶ bound of lem:aniso:closure #
The spatial L⁶ bound on the ball B(ρ), from the weighted enstrophy bound.
If χ is a smooth cutoff supported in the open set U on whose time slices u is smooth and
divergence free, χ = 1 on B(ρ), |u(·,t)| ≤ Mu wherever ∇χ ≠ 0, and the enstrophy
Y t = ∫ χ² |curl u(·,t)|² satisfies Y t + 1 ≤ C' (-t)^(-a) on (tη, 0), then
‖u(·,t)‖_{L⁶(B(ρ))} ≤ C'' (-t)^(-a/2) on (tη, 0).
The (-t)-exponent is halved because the gradient energy enters through its square root.
The closure of lem:aniso:closure #
The closure step: with η = 1 / (16 C_*) the enstrophy bound of closure_gronwall_bound
yields exactly the parabolic smallness hypothesis of the Gustafson–Kang–Tsai criterion
gktCriterion.
The exponent bookkeeping is the point. The enstrophy decays like (-t)^(-C_* η), so the L⁶
norm decays like (-t)^(-β) with β = C_* η / 2. The L⁴_t L⁶_x quantity of the criterion
raises this to the fourth power and integrates in time over (-r², 0), which converges and
carries a positive power of r exactly when 4β < 1. With η = 1 / (16 C_*) one has
C_* η = 1/16, hence β = 1/32 and 4β = 1/8 < 1.