The tested enstrophy balance eq:aniso:closure:tested #
This file proves the differential inequality eq:aniso:closure:tested of
Regularity of asymptotically axisymmetric solutions to the 3D Navier–Stokes equations with
analytic forcing, arXiv:2609.20803.
Let u be a classical solution on the unit cylinder, ω = curl u its Cartesian vorticity
(vorticityField), and χ a smooth cutoff whose support is a compact subset of the unit
ball. With
Y t = ∫ χ² |ω(·, t)|², M t = ∫ χ² |∇ω(·, t)|²,
the vorticity equation cartesian_vorticity_pde tested against χ² ω gives
½ Y' + M ≤ ∫ χ² (ω·∇u)·ω + C (Y + 1).
The three tested terms are recorded separately:
- the transport term is
∫ χ² ω·(u·∇ω) = -½ ∫ |ω|² u·∇(χ²); the divergence-free condition removes the termχ² (div u) |ω|², and the right-hand side is supported where∇χ ≠ 0; - the diffusion term is
∫ χ² ω·Δω = -M + ½ ∫ |ω|² Δ(χ²), obtained by two integrations by parts, so that the cutoff error only seesωitself and not∇ω; - the force term obeys
|∫ χ² ω·curl f| ≤ C (Y + 1), sincecurl fis bounded by twice theC²bound of the force.
Every integration by parts is an instance of
integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable: the cutoff-carrying factor is globally
smooth with compact support, so the other factor — built from u and its derivatives — only
has to be differentiable on the unit ball.
This module carries the time differentiation of Y and the three tested terms; the resulting
differential inequality is assembled in CIV.Closure.EnstrophyBalance.
The cutoff-weighted quantities #
The cutoff enstrophy Y t = ‖χ ω(·, t)‖_{L²}² of lem:aniso:closure.
Equations
- CIV.cutoffEnstrophy χ u t = ∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * ∑ i : Fin 3, CIV.vorticityField u (x, t) i ^ 2
Instances For
The cutoff enstrophy dissipation M t = ‖χ ∇ω(·, t)‖_{L²}² of lem:aniso:closure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The tested vortex-stretching term ∫ χ² (ω·∇u)·ω of eq:aniso:closure:tested.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Cutoff weights and fields smooth on an open set #
A weight is a globally smooth, compactly supported scalar whose support lies inside the
open set U on which the velocity is smooth. Weight times U-smooth field is globally
continuous with compact support, hence integrable; this is what makes every integration by
parts below legitimate.
Two elementary derivative rules #
Integrating a finite sum, and integrability under a cutoff #
A function continuous on the unit ball and vanishing off the support of the cutoff is integrable.
The square of a cutoff #
Slices of the velocity and of the vorticity #
The repo's classical partial derivatives are read on a time slice: spatialPartial g j (x, t)
is fderiv ℝ (fun y => g (y, t)) x (basisVec j) by definition, and vorticityField u z i is
curlComp u i z. The proofs below work with the fderiv form throughout.
Differentiating the enstrophy under the integral sign #
Stage (i) of eq:aniso:closure:tested. The cutoff enstrophy is differentiable in
time and its derivative is obtained by differentiating under the integral sign. The
domination is uniform on a compact time slab inside the cylinder, where ω and ∂_t ω are
bounded by continuity, and the cutoff makes the spatial support compact.
Continuity of the slice quantities #
The time slice of a component of the curl is continuous on the unit ball.
A spatial derivative of the vorticity is continuous on the unit ball.
A second spatial derivative of the vorticity is continuous on the unit ball.
The time slice of a component of the velocity is continuous on the unit ball.
A spatial derivative of the velocity is continuous on the unit ball.
Stage (ii)(a): the transport term #
The tested transport term of eq:aniso:closure:tested. Testing u·∇ω against χ² ω
and integrating by parts gives ∫ χ² ω·(u·∇ω) = -½ ∫ |ω|² u·∇(χ²); the term
½ ∫ χ² (div u) |ω|² produced by the product rule vanishes because u is divergence free.
The right-hand side is supported where ∇χ ≠ 0.
Stage (ii)(b): the diffusion term #
The tested diffusion term of eq:aniso:closure:tested. Testing Δω against χ² ω
and integrating by parts twice gives ∫ χ² ω·Δω = -M + ½ ∫ |ω|² Δ(χ²). The second
integration by parts moves the surviving derivative off ∇ω, so that the cutoff error only
involves ω itself on the annulus where χ is not locally constant.
Stage (ii)(c): the force term #
The tested force term of eq:aniso:closure:tested. Since curl f is bounded by twice
the C² bound eq:interior:force:c-two of the force, the tested force term obeys
|∫ χ² ω·curl f| ≤ C (Y + 1) with a constant depending only on that bound and on χ, on the
time window (t₀, 0).
Stage (ii)(d): the two cutoff errors are bounded #
The transport cutoff error is bounded. The term ½ ∫ |ω|² u·∇(χ²) produced by the
transport integration by parts is supported where ∇χ ≠ 0, so the bounds for |u| and |ω|
there, on the time window (t₀, 0), make it a constant.
The diffusion cutoff error is bounded. The term ½ ∫ |ω|² Δ(χ²) left by the second
integration by parts sees only ω itself, on the set where χ is not locally constant, and
on the time window (t₀, 0).