Sobolev Poincare Bridge

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

noncomputable def CKN.sobolevPoincareBallFullConstant : ENNReal

Volume-normalization coefficient for the full ball Sobolev estimate.

Equations

• CKN.sobolevPoincareBallFullConstant = ENNReal.ofReal (Real.pi * 4 / 3) ^ (-(1 / 3))

theorem CKN.vector_h1_sobolev_ball_integral {x₀ : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) (u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3) (hu : Fin 3 → H1Function (euclideanBall x₀ r)) (hcomp : ∀ (i : Fin 3), (hu i).toFun = fun (x : Foundation.Parabolic.Vec3) => u x i) (hgrad : ∀ (i : Fin 3), (hu i).grad = fun (x : Foundation.Parabolic.Vec3) => D x i) : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => u y i - ⨍ (z : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, u z i) 6 (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ r)) ∧ (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, (Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => u y i - ⨍ (z : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, u z i) ^ 6) ^ (1 / 6) ≤ 9 * sobolevPoincareL6Constant.toReal * (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, ∑ i : Fin 3, ∑ j : Fin 3, D y i j ^ 2) ^ (1 / 2)

The scalar weak Sobolev estimate aggregated over the three velocity components.

theorem CKN.h1SobolevBall_of_sobolevPoincare {x₀ : Vec 3} {r : ℝ} (hr : 0 < r) (u : H1Function (euclideanBall x₀ r)) : lpNormOn 6 (euclideanBall x₀ r) u.toFun ≤ (2 * sobolevPoincareL6Constant + 2 * sobolevPoincareBallFullConstant) * (weakGradientLpNormOn 2 (euclideanBall x₀ r) u.grad + (ENNReal.ofReal r)⁻¹ * lpNormOn 2 (euclideanBall x₀ r) u.toFun)