Energy Class Lemmas

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.lintegral_gradSq_lt_top {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 → ℝ} (h : GlobalEnergyClass u Du p) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in unitCylinder, ‖Du z‖ₑ ^ 2 < ⊤

theorem CIV.exists_bound_of_forceC2Bounded {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : ForceC2Bounded f) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ z ∈ unitCylinder, CKN.Foundation.Parabolic.vec3EuclideanNorm (f z) ≤ M

A C²-bounded force is bounded in Euclidean norm on the unit cylinder.

theorem CIV.exists_component_bound_of_forceC2Bounded {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : ForceC2Bounded f) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ z ∈ unitCylinder, ∀ (i : Fin 3), |f z i| ≤ M

A C²-bounded force is bounded componentwise on the unit cylinder.