The right-hand integrand of the local energy inequality #
The local energy inequality of def:sws carries a second integrability side
condition, on the integrand of its right-hand side. That integrand has three
groups of terms, all of them tested against the closed support of the test
function ψ:
- the heat-operator term
|u|² (∂ₜψ + Δψ); - the flux term
(|u|² + 2p) (u · ∇ψ); - the force term
2 (f · u) ψ.
This file proves that side condition from the data clauses alone.
The first group needs only that the velocity is square integrable on a compact
set, which the finite joint energy of the data clauses already gives. The other
two are the reason the parabolic interpolation of
CKN/ClassEquivalence/VelocityTenThirds.lean is needed at all: the cubic
density |u|² uᵢ and the pressure-velocity density p uᵢ are not controlled by
square integrability, and are obtained there from the local L³ bound on the
velocity, the pressure exponent 3 / 2 and the Hölder pairing 2 / 3 + 1 / 3 = 1.
The force term uses the same pairing, the force exponent of def:sws being
larger than 3 / 2.
Each group is then an integrable density times a bounded derivative of the test
function, and the three are added. The energy density of the paper is the
Euclidean norm CKN.Foundation.Parabolic.vec3EuclideanNorm, while the data
clauses are stated with the supremum norm of Vec3; only the easy direction of
the equivalence of the two norms is used.
Nothing about the identities of def:sws is used, so the conclusion is
available while those identities are still being established. In particular the
nonnegativity of the test function that the clause also assumes is not
needed for integrability and is omitted here.
The densities of the right-hand side on a compact set #
The energy density |u|² of the local energy inequality is integrable on
every compact subset of the space-time carrier: the velocity is square
integrable there by the data clauses.
The cubic density |u|² uᵢ of the flux term is integrable on every compact
subset of the space-time carrier: it is bounded in absolute value by |u|³,
which the parabolic interpolation controls there.
The whole density (|u|² + 2p) uᵢ of the flux term of the local energy
inequality is integrable on every compact subset of the space-time carrier.
The density f · u of the force term of the local energy inequality is
integrable on every compact subset of the space-time carrier.
The three groups of terms #
The heat-operator term |u|² (∂ₜψ + Δψ) of the right-hand side is
integrable on a compact subset of the carrier.
The flux term (|u|² + 2p) (u · ∇ψ) of the right-hand side is integrable on
a compact subset of the carrier.
The force term 2 (f · u) ψ of the right-hand side is integrable on a
compact subset of the carrier.
The right-hand integrand #
The integrand of the right-hand side of the local energy inequality of
def:sws is integrable on the closed support of the test function. Only the
data clauses are used, so the conclusion is available while the identities of
def:sws are still being established.