Reading off the compactness conclusions

lem:compactness of the CKN manuscript states its conclusions in Hilbert-valued L² spaces. These lemmas convert them into the coordinate pairings, the coordinate L² distances, and the gradient integrability used in prop:blowup-limit.

theorem ESS.blowupLimitAssembly_inner_eq_pairing {C : Set CKN.Foundation.Parabolic.Vec3} (u ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hψC : ∀ x ∉ C, ψ x = 0) (hu : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u x)) 2 (MeasureTheory.volume.restrict C)) (hψ : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => WithLp.toLp 2 (ψ x)) 2 (MeasureTheory.volume.restrict C)) : inner ℝ (MeasureTheory.MemLp.toLp (fun (x : CKN.Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u x)) hu) (MeasureTheory.MemLp.toLp (fun (x : CKN.Foundation.Parabolic.Vec3) => WithLp.toLp 2 (ψ x)) hψ) = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u x i * ψ x i

The Hilbert pairing of two vector slices on a set carrying the second slice is the whole-space coordinate pairing.

theorem ESS.blowupLimitAssembly_integrable_pairing {C : Set CKN.Foundation.Parabolic.Vec3} (u ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hψC : ∀ x ∉ C, ψ x = 0) (hu : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u x)) 2 (MeasureTheory.volume.restrict C)) (hψ : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => WithLp.toLp 2 (ψ x)) 2 (MeasureTheory.volume.restrict C)) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, u x i * ψ x i) MeasureTheory.volume

A vector slice in L² of a set pairs integrably with a test carried by that set.

theorem ESS.blowupLimitAssembly_norm_sub_le (a b : CKN.Foundation.Parabolic.Vec3) : ‖a - b‖ ≤ ‖WithLp.toLp 2 a - WithLp.toLp 2 b‖

The coordinate sup norm is dominated by the Euclidean norm of the Hilbert copy.

theorem ESS.blowupLimitAssembly_norm_sq_le_spatialGradientSq (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ‖Du z‖ ^ 2 ≤ CKN.spatialGradientSq u Du z

The sup norm of a gradient matrix is controlled by its energy density.

theorem ESS.blowupLimitAssembly_memLp_gradient_of_energy (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hDu : Measurable Du) (C : Set CKN.Foundation.Parabolic.Vec3) (a b : ℝ) (hfin : ∫⁻ (t : ℝ) in Set.Icc a b, ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (CKN.spatialGradientSq u Du (x, t)) < ⊤) (Q : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)) (hQ : Q ⊆ C ×ˢ Set.Icc a b) : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict Q)

A measurable gradient with finite iterated energy on a product set is square integrable on every subset.