Sobolev Six

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

theorem CIV.exists_sobolev_six_const : ∃ (C : ℝ), 0 < C ∧ ∀ (g : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ 1 g → HasCompactSupport g → MeasureTheory.eLpNorm g 6 MeasureTheory.volume ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm (fderiv ℝ g) 2 MeasureTheory.volume

The Sobolev inequality in ℝ³ for compactly supported C¹ functions: L⁶ norm bounded by L² norm of the derivative, with an explicit constant.

We use eLpNorm (the Lᵖ norm in the sense of extended nonnegative reals) because converting to explicit real-valued integrals would require additional measure-theoretic identifications.

theorem CIV.exists_sobolev_six_const_vec : ∃ (C : ℝ), 0 < C ∧ ∀ (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), (∀ (i : Fin 3), ContDiff ℝ 1 fun (x : CKN.Foundation.Parabolic.Vec3) => v x i) → (∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => v x i) → ∑ i : Fin 3, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => v x i) 6 MeasureTheory.volume ≤ ENNReal.ofReal C * ∑ i : Fin 3, MeasureTheory.eLpNorm (fderiv ℝ fun (x : CKN.Foundation.Parabolic.Vec3) => v x i) 2 MeasureTheory.volume

Vector-field version of the Sobolev inequality in ℝ³. Applied componentwise to v : Vec3 → Vec3 with each component C¹ and compactly supported.