The three main theorems under the manuscript's hypothesis #
Definition def:sws of the manuscript asks four things of a suitable weak
solution: the regularity class (S1), the divergence-free identity (S2), the
weak momentum identity (S3) and the local energy inequality (S4). It attaches
no integrability side condition to (S2), (S3) or (S4); the integrals appearing
there are simply asserted to vanish, or to satisfy an inequality.
CKN.IsSuitableWeakSolution of CKN/Statements/SuitableWeakSolution.lean
transcribes that definition literally, and it is the hypothesis of the
statements of Theorems A, B and C.
The Lean class CKN.IsSuitableWeakSolutionIntegrable states the same four conditions but
carries, inside its (S2), (S3) and (S4) clauses, four IntegrableOn
conjuncts - one for the divergence-free integrand, one for the momentum
integrand, and one for each side of the local energy inequality. They were
recorded there because the Bochner integral of a non-integrable function is 0
by convention: an identity ∫ ... = 0 read off a non-integrable integrand is
true for the wrong reason, and a class that allowed that would be weaker than
the manuscript's.
Those four conjuncts are not extra assumptions. The files
CKN/ClassEquivalence/*.lean derive each of them from the (S1) clauses alone,
and CKN.isSuitableWeakSolutionIntegrable_iff_identities assembles that derivation into
an equivalence. So the class with the side conditions and the class without
them have exactly the same inhabitants; CKN.isSuitableWeakSolution_iff_integrable
records the identification.
The three theorems that follow are Theorem A, Theorem B and Theorem C under the
manuscript's hypothesis. Each is the corresponding implementation export of
CKN/Main/TheoremA.lean, CKN/Main/TheoremB.lean and CKN/Main/TheoremC.lean,
whose hypothesis is CKN.IsSuitableWeakSolutionIntegrable, composed with the equivalence;
the conclusions are copied unchanged. CKN/Main/TheoremAPaper.lean,
CKN/Main/TheoremBPaper.lean and CKN/Main/TheoremCPaper.lean re-export them,
and the statements are short assemblies of those re-exports.
Both forms of the class therefore exist, and both are wanted. The development
proves its intermediate results with CKN.IsSuitableWeakSolutionIntegrable, which keeps
the integrability of each tested integrand visible at the point of use. The
statements assume CKN.IsSuitableWeakSolution: exactly what
def:sws assumes, and nothing more.
The manuscript's suitable weak-solution class and the class carrying the
integrability side conditions have the same inhabitants. Read from left to
right this is the content of CKN/ClassEquivalence: the four IntegrableOn
conjuncts of CKN.IsSuitableWeakSolutionIntegrable follow from the (S1) clauses, so
assuming them assumes nothing beyond def:sws. Read from right to left it is
the projection that discards them.
The two classes group their clauses differently - CKN.IsSuitableWeakSolutionIntegrable
and CKN.IsSuitableWeakSolution both write the (S1) clauses inline, while
CKN.isSuitableWeakSolutionIntegrable_iff_identities collects them into
CKN.IsSuitableWeakSolutionData - so each direction re-associates the
conjunction before handing it on. No identity is read at a junk value of the
Bochner integral: the left-to-right direction goes through
CKN.isSuitableWeakSolutionIntegrable_of_identities, which establishes the four
integrability clauses from the (S1) clauses before consuming any identity.
Theorem A of the manuscript, paper label thm:A, under the manuscript's
definition of a suitable weak solution. The conclusion is that of
CKN.epsilonRegularityL3, unchanged; the hypothesis class of the implementation
export CKN.Main.epsilonRegularityL3 differs, and by
CKN.isSuitableWeakSolution_iff_integrable the two classes coincide.
Theorem B of the manuscript, paper label thm:B, under the manuscript's
definition of a suitable weak solution. The conclusion is that of
CKN.epsilonRegularityGradient, unchanged; the hypothesis class of the
implementation export CKN.Main.epsilonRegularityGradient differs, and by
CKN.isSuitableWeakSolution_iff_integrable the two classes coincide.
Theorem C of the manuscript, paper label thm:C, under the manuscript's
definition of a suitable weak solution. The conclusion is that of
CKN.caffarelliKohnNirenberg, unchanged; the hypothesis class of the
implementation export CKN.Main.caffarelliKohnNirenberg differs, and by
CKN.isSuitableWeakSolution_iff_integrable the two classes coincide.