Poincare Sobolev L1 Vec

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

noncomputable def CKN.poincareSobolevL1VectorConstant : ℝ

Explicit constant for the vector-valued ball inequality.

Equations

• CKN.poincareSobolevL1VectorConstant = 2 * √3 * CKN.poincareSobolevL1Constant.toReal

theorem CKN.poincareSobolevL1_vec3_ball (x₀ : Foundation.Parabolic.Vec3) {r : ℝ} (hr : 0 < r) (u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hu : ContDiff ℝ 1 u) : (∫ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, |Foundation.Parabolic.vec3EuclideanNorm (u x) ^ 2 - ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, Foundation.Parabolic.vec3EuclideanNorm (u y) ^ 2| ^ (3 / 2)) ^ (2 / 3) ≤ poincareSobolevL1VectorConstant * (∫ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, Foundation.Parabolic.vec3EuclideanNorm (u x) ^ 2) ^ (1 / 2) * (∫ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, ∑ i : Fin 3, ∑ j : Fin 3, (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => u y i) x) (basisVec j) ^ 2) ^ (1 / 2)

Vector-valued Poincare–Sobolev inequality for a continuously differentiable map.