The two forms of the suitable weak-solution class

CKN.IsSuitableWeakSolution is the suitable weak-solution class as the CKN manuscript states it, and it is the class the statements of this repository assume. The CKN library proves its estimates for CKN.IsSuitableWeakSolutionIntegrable, which adds an integrability condition to each identity clause. The two classes have the same inhabitants: the extra conditions follow from the measurability and local integrability clauses (CKN.isSuitableWeakSolutionIntegrable_of_identities). This file records both directions for use at the calls into the CKN library.

theorem CIV.isSuitableWeakSolutionIntegrable_of_isSuitableWeakSolution {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : CKN.IsSuitableWeakSolution Ω I q u Du p f) : CKN.IsSuitableWeakSolutionIntegrable Ω I q u Du p f

A suitable weak solution in the sense of the CKN manuscript satisfies the integrability conditions that the CKN library carries in its class.

theorem CIV.isSuitableWeakSolution_of_integrable {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : CKN.IsSuitableWeakSolutionIntegrable Ω I q u Du p f) : CKN.IsSuitableWeakSolution Ω I q u Du p f

Dropping the integrability conditions of the CKN library class gives a suitable weak solution in the sense of the CKN manuscript.