Poincare Sobolev L1 Ball

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

def CKN.euclideanAffineMap (x₀ : Vec 3) (r : ℝ) (x : Vec 3) : Vec 3

Translation and dilation map transporting unit-ball inequalities to arbitrary balls.

Equations

• CKN.euclideanAffineMap x₀ r x = x₀ + r • x

theorem CKN.poincareSobolevL1_ball (x₀ : Vec 3) {r : ℝ} (hr : 0 < r) (g : Vec 3 → ℝ) (hg : ContDiff ℝ 1 g) : (∫ (x : Vec 3) in euclideanBall x₀ r, |g x - integralAverage (euclideanBall x₀ r) g| ^ (3 / 2)) ^ (2 / 3) ≤ poincareSobolevL1Constant.toReal * ∫ (x : Vec 3) in euclideanBall x₀ r, ‖fderiv ℝ g x‖