Documentation

LeanPool.NavierStokesAndEuler.NavierStokes.R3.WholeSpaceUniqueness

Whole-space finite-energy comparison #

The reference velocity has one compact spatial support throughout the closed time interval. The competing velocity has only smoothness and a uniform finite-energy bound. No growth, decay, support or derivative bound is assumed for the competing pressure or velocity. The pressure flux estimate is derived from the actual equation by the imported pressure recovery and commutator theorems.

Closing the whole-space comparison estimate #

This module isolates the final PDE energy calculation. Its explicit pressure flux hypothesis is discharged by the pressure reconstruction modules in the whole-space uniqueness theorem; it is not a competitor hypothesis.

The compactly weighted difference-energy identity on R³ #

The cutoff alone has compact support. Both velocities and both pressures may be arbitrary smooth fields on the time slab. Every integral below is an ordinary Lebesgue volume integral on Euclidean three-space.

The Laplacian in a compactly weighted energy identity #

All integrals are ordinary volume integrals on Euclidean three-space. The weight is smooth and compactly supported; the vector field is smooth but is not required to have compact support or globally integrable derivatives.

A uniform rate bound from the localized energy estimate #

The Sobolev estimate for the cutoff velocity contains fixed multiplicative constants. They are absorbed into a single coefficient before applying the uniform Young estimate. The resulting error decays as 1 / R, and no sign condition on the energy coefficient or energy value is used.

Scalar absorption for the whole-space comparison estimate #

The constants in these estimates are uniform in the cutoff radius and in the nonnegative quantity that will represent a weighted gradient norm. All fractional powers have real exponents.

Non-pressure terms in the localized difference energy balance #

The velocity difference need not have compact support or globally integrable derivatives. The compact cutoff supplies local integrability; the estimates use its weighted L⁶ norm and the unweighted L² norm of the difference.

Scalar closure of the whole-space comparison estimate #

The localized energy may have derivatives only in the interior of the time interval. The shared scalar Gronwall estimates therefore use continuity on the closed interval and derivatives on its interior. In particular, no energy inequality at a time endpoint is assumed.

Removing the spatial energy cutoff #

At a fixed time, square integrability gives an integrable dominating function. This module removes the cutoff only after that hypothesis has been supplied.

Constants supplied by the compactly supported comparison solution #

These bounds are consequences of joint smoothness and one fixed compact spatial support. They impose no condition on the competing solution.