Sobolev Poincare Ball Weak

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

theorem CKN.sobolevPoincare_L6_ball_weak_inner (x₀ : Vec 3) {r s : ℝ} (hr : 0 < r) (hs : 0 < s) (hsr : s < r) (u : H1Function (euclideanBall x₀ r)) : (lpNormOn 6 (euclideanBall x₀ s) fun (x : Vec 3) => u.toFun x - MeasureTheory.average (MeasureTheory.volume.restrict (euclideanBall x₀ s)) u.toFun) ≤ sobolevPoincareL6Constant * weakGradientLpNormOn 2 (euclideanBall x₀ s) u.grad

theorem CKN.sobolevPoincare_L6_ball_weak (x₀ : Vec 3) {r : ℝ} (hr : 0 < r) (u : H1Function (euclideanBall x₀ r)) : (lpNormOn 6 (euclideanBall x₀ r) fun (x : Vec 3) => u.toFun x - MeasureTheory.average (MeasureTheory.volume.restrict (euclideanBall x₀ r)) u.toFun) ≤ sobolevPoincareL6Constant * weakGradientLpNormOn 2 (euclideanBall x₀ r) u.grad