Quadratic sum of cutoff data

Global L² bounds imply finiteness of the four-term quadratic integral required by the Sobolev half-space Carleman estimate.

theorem ESS.bu_memLp_four_sum_lintegral_lt_top (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hDw : MeasureTheory.MemLp Dw 2 MeasureTheory.volume) (hD2w : MeasureTheory.MemLp D2w 2 MeasureTheory.volume) (hDtw : MeasureTheory.MemLp Dtw 2 MeasureTheory.volume) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤

Four globally square-integrable weak data fields have finite summed quadratic energy on any measurable subregion.