eq:aniso:closure:elliptic in the tested quantities Y and M #
This file states the two elliptic bounds of lem:aniso:closure in the form the mixed-term
estimate eq:aniso:closure:mixed:bound consumes them: with the cutoff χ of the closure
argument and a classical solution u on the unit cylinder,
∫ χ² |∇u(·, t)|² ≤ C (Y t + 1) and ∫ χ² |∇²u(·, t)|² ≤ C (M t + 1),
where Y = cutoffEnstrophy χ u and M = cutoffEnstrophyDissipation χ u. Both are stated in the
spatialPartial/spatialSecondPartial operators of the classical formulation and share the
hypothesis block of energy_inequality_of_mixed_term_bound, so the two families compose.
Following the convention of this formalization, the bounds are carried by the full velocity u
rather than by the meridional velocity b = u_r e_r + u_z e_z of the printed argument: the
pointwise dominations |∂_r u_z| ≤ |∇u| and |∂_z∂_r u_z| ≤ |∇²u| replace |∂_r u_z| ≤ |∇b|
and |∂_z∂_r u_z| ≤ |∇²b|, and the two inequalities come out with the same Y and M.
The three inputs taken as hypotheses #
The two bounds of this file take three inequalities that lem:aniso:closure uses as explicit,
named hypotheses. Each is stated exactly as the lemma that proves it, and
CIV.Closure.EllipticBoundsAnnulusBound discharges all three by one application each:
hCommutatorFirst by integral_cutoff_sq_fderiv_le, hCommutatorSecond by
integral_cutoff_sq_fderiv_fderiv_le, and hEllipticSecond by
integral_sq_fderiv_fderiv_smul_le. The closure lemma therefore carries none of them.
hCommutatorFirst— the first-order cutoff commutator‖χ∇v‖² ≤ 2‖∇(χv)‖² + 2 N²‖∇χ‖², which moves the cutoff across one derivative at the cost of a term supported where∇χ ≠ 0.hCommutatorSecond— its second-order counterpart‖χ∇²v‖² ≤ 4‖∇²(χv)‖² + 16 N²(‖∇χ‖² + ‖∇²χ‖²).hEllipticSecond— the second elliptic bound‖∇²(χv)‖² ≤ 4‖χ∇curl v‖² + 24 N²(‖∇χ‖² + ‖∇²χ‖²), the second-order analogue of theintegral_sq_fderiv_smul_le, obtained from the second-order form of the div–curl identityeq:aniso:closure:ellipticapplied toχ v.
All three carry the regularity block of integral_sq_fderiv_smul_le — U open, χ smooth with
compact support inside U, v smooth on U. That block is not decoration: without it the three
integrals on the right need not be finite, a Bochner integral of a non-integrable function is
zero, and each inequality is then false. With it all three are true, and all three are applied
below at data for which every one of those regularity hypotheses is supplied by the hypothesis
block of the theorems themselves.
The first elliptic bound is the integral_sq_fderiv_smul_le, and the two identifications
of the cutoff-weighted curl energies with Y and M are proved here.
Where the derivatives of the cutoff live #
The gradient of a cutoff is supported in the support of the cutoff.
A closed set outside which the cutoff has vanishing derivative contains the support of the gradient of the cutoff. This is the shape in which the closure argument records where the cutoff error terms live.
The tested quantities as curl energies #
Y t = ‖χ ω(·, t)‖² is the cutoff-weighted L² norm of the curl of the time slice of u.
M t = ‖χ ∇ω(·, t)‖² is the cutoff-weighted L² norm of the gradient of the curl of the
time slice of u.
Reading the classical operators off the time slice #
Elementary bounds #
The two bounds of eq:aniso:closure:elliptic #
The gradient half of eq:aniso:closure:elliptic. For a classical solution on the unit
cylinder and a cutoff supported in the unit ball, the cutoff-weighted gradient energy of the
velocity is bounded by C (Y + 1), with Y = cutoffEnstrophy χ u the tested enstrophy. The
hypothesis block is that of energy_inequality_of_mixed_term_bound; hCommutatorFirst is the
one addition.
The Hessian half of eq:aniso:closure:elliptic. For a classical solution on the unit
cylinder and a cutoff supported in the unit ball, the cutoff-weighted Hessian energy of the
velocity is bounded by C (M + 1), with M = cutoffEnstrophyDissipation χ u the tested
enstrophy dissipation. The hypothesis block is that of energy_inequality_of_mixed_term_bound,
extended by hubd2 — the derivative bound of lem:aniso:annulus, in the exact shape
regularAnnulus produces it — and by the two carried inequalities hCommutatorSecond and
hEllipticSecond.