The integrability clauses of def:sws are redundant

Each of the three identity clauses of CKN.IsSuitableWeakSolutionIntegrable pairs an identity with an integrability side condition on the integrand that identity tests; the local energy inequality carries two such side conditions, one for each side. The four preceding files prove all four of them from the data clauses alone. This file puts them together: to exhibit a suitable weak solution it is enough to supply the data clauses and the three bare identities.

Why the order of the proof matters

The Bochner integral of a function that is not integrable is 0 by convention. An identity such as ∫ z in spaceTimeSet Ω I, ∑ i, u z i * ∂ᵢψ z = 0 therefore says nothing on its own: it also holds, vacuously, when the integrand is not integrable. A constructor that consumed such an identity before knowing the integrand to be integrable would be proving the class from a hypothesis that is weaker than it looks.

CKN.isSuitableWeakSolutionIntegrable_of_identities avoids this. It calls the four clause lemmas first, and those lemmas read only the data clauses; they never look at the value of an integral. By the time each identity is consumed its integrand is already known to be integrable, so the integral appearing in it is a genuine Bochner integral and not the junk value.

For the same reason the identities are stated here with the integral written exactly as the clauses write it, over spaceTimeSet Ω I. No transport between forms of the integral is then needed, and the proof below is a plain rearrangement of conjunctions. A caller who holds an identity in another form, for instance over the closed support of the test function or over the whole space-time, has to transport it, and that transport is legal only once the integrability is in hand - which is exactly what these lemmas supply.

theorem CKN.isSuitableWeakSolutionIntegrable_of_identities {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hdata : IsSuitableWeakSolutionData Ω I q u Du p f) (hdiv : ∀ ψ ∈ spaceTimeTestFunction Ω I, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, ∑ i : Fin 3, u z i * spatialPartial ψ i z = 0) (hmom : ∀ φ ∈ spaceTimeTestFunction Ω I, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, -∑ i : Fin 3, u z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z - p z * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z - ∑ i : Fin 3, f z i * φ z i = 0) (hlei : ∀ ψ ∈ spaceTimeTestFunction Ω I, (∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ ψ z) → 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, spatialGradientSq u Du z * ψ z ≤ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + (Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 + 2 * p z) * ∑ i : Fin 3, u z i * spatialPartial ψ i z + (2 * ∑ i : Fin 3, f z i * u z i) * ψ z) : IsSuitableWeakSolutionIntegrable Ω I q u Du p f

The data clauses of def:sws together with the three bare identities - the divergence-free identity, the weak momentum identity and the local energy inequality, each stated without its integrability side condition - already give a suitable weak solution.

The four integrability side conditions of the class are supplied by the clause lemmas, which use the data clauses only. They are established before any of hdiv, hmom and hlei is consumed, so no identity here is read at a junk value of the Bochner integral.

theorem CKN.isSuitableWeakSolutionIntegrable_iff_identities {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} : IsSuitableWeakSolutionIntegrable Ω I q u Du p f ↔ IsSuitableWeakSolutionData Ω I q u Du p f ∧ (∀ ψ ∈ spaceTimeTestFunction Ω I, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, ∑ i : Fin 3, u z i * spatialPartial ψ i z = 0) ∧ (∀ φ ∈ spaceTimeTestFunction Ω I, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, -∑ i : Fin 3, u z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z - p z * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z - ∑ i : Fin 3, f z i * φ z i = 0) ∧ ∀ ψ ∈ spaceTimeTestFunction Ω I, (∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ ψ z) → 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, spatialGradientSq u Du z * ψ z ≤ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + (Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 + 2 * p z) * ∑ i : Fin 3, u z i * spatialPartial ψ i z + (2 * ∑ i : Fin 3, f z i * u z i) * ψ z

The suitable weak-solution class of def:sws is equivalent to its data clauses together with the three bare identities. This is the precise sense in which the four integrability conjuncts of the class are redundant: they are consequences of the measurability and local integrability recorded by the data clauses, and carrying them in the definition assumes nothing extra.