Vector Norm Aggregation

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

Aggregation of componentwise vector inequalities to the Euclidean norm

The Poincare and H¹ interpolation inequalities of CKN.Setting.VectorInequalities are stated componentwise: each coordinate u_i of a velocity field u : Vec3 → Vec3 is controlled by the scalar theorems. The estimates of paper/ckn.tex instead use the Euclidean norm |u| and the Frobenius norm of the spatial gradient, |∇u|² = spatialGradientSq. This file supplies the finite-dimensional norm comparisons that turn the componentwise statements into their Euclidean counterparts.

The two elementary inequalities on ℝ³ are

• |u|^p ≤ 3^{max(0,p/2-1)} Σ_i |u_i|^p (the sharp comparison of the Euclidean norm with the component ℓᵖ mass), and
• Σ_i |u_i|^p ≤ 3 |u|^p.

Both are proved pointwise and then integrated, first on the ℝ≥0∞ side (the form in which the scale quantities γ, α, β store their local Lᵖ masses) and then for the spatial balls used by the Poincare and Sobolev statements.

Pointwise comparison on ℝ³

theorem CKN.vec3EuclideanNorm_rpow_le_sum_rpow (x : Foundation.Parabolic.Vec3) {p : ℝ} (hp : 1 ≤ p) : Foundation.Parabolic.vec3EuclideanNorm x ^ p ≤ 3 ^ max 0 (p / 2 - 1) * ∑ i : Fin 3, |x i| ^ p

The Euclidean norm raised to p ≥ 1 is controlled by the component ℓᵖ mass with the sharp finite-dimensional constant: |u|^p ≤ 3^{max(0,p/2-1)} Σ_i |u_i|^p.

The ℝ≥0∞ integrable form used by the scale quantities

theorem CKN.ofReal_vec3EuclideanNorm_rpow_le_sum {u : Foundation.Parabolic.Vec3} {p : ℝ} (hp : 1 ≤ p) : ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm u) ^ p ≤ ENNReal.ofReal (3 ^ max 0 (p / 2 - 1)) * ∑ i : Fin 3, ‖u i‖ₑ ^ p

Pointwise comparison on the ℝ≥0∞ side: the p-th power of the Euclidean density is dominated by the component ℓᵖ mass with the sharp finite-dimensional constant.

theorem CKN.lintegral_vec3EuclideanNorm_rpow_le_sum {s : Set Foundation.Parabolic.Vec3} {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {p : ℝ} (hp : 1 ≤ p) (hu : ∀ (i : Fin 3), AEMeasurable (fun (x : Foundation.Parabolic.Vec3) => u x i) (MeasureTheory.volume.restrict s)) : ∫⁻ (x : Foundation.Parabolic.Vec3) in s, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u x)) ^ p ≤ ENNReal.ofReal (3 ^ max 0 (p / 2 - 1)) * ∑ i : Fin 3, ∫⁻ (x : Foundation.Parabolic.Vec3) in s, ‖u x i‖ₑ ^ p

Integrated form of the sharp comparison: the Lᵖ mass of the Euclidean density is controlled by the sum of the component Lᵖ masses.