Poincare Sobolev L1 Slice

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

theorem CKN.poincareSobolevL1_vec3_slice_euclidean {U : Set Foundation.Parabolic.Vec3} (hU : IsOpen U) {x₀ : Foundation.Parabolic.Vec3} {R r : ℝ} (hr : 0 < r) (hrr : r < R) (hball : Foundation.Parabolic.vec3Ball x₀ R ⊆ U) (u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (g : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3) (hu : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u x i) 2 (MeasureTheory.volume.restrict U)) (hg : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => g x i) 2 (MeasureTheory.volume.restrict U)) (hweak : ∀ (i : Fin 3), HasWeakGradientOn U (fun (x : Vec 3) => u x i) fun (x : Vec 3) => g x i) : (∫ (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, g x i j ^ 2) ^ (1 / 2)

H¹ lift of the vector-valued Poincare–Sobolev inequality on nested balls.