Approximation lemmas for Sobolev–Poincaré on Euclidean balls

These lemmas transfer smooth Euclidean-ball Poincaré estimates to W¹,¹ data.

theorem CKN.w1p_euclideanBall_poincareL1_faithful (x₀ : Foundation.Parabolic.Vec3) {r : ℝ} (hr : 0 < r) (u : W1pFunction (euclideanBall x₀ r) 1) : ∫ (x : Vec 3) in euclideanBall x₀ r, |u.toFun x - MeasureTheory.average (MeasureTheory.volume.restrict (euclideanBall x₀ r)) u.toFun| ≤ poincareSobolevL1Constant.toReal * (MeasureTheory.volume (euclideanBall x₀ r)).toReal ^ (1 / 3) * ∫ (x : Vec 3) in euclideanBall x₀ r, w1pGradientNorm u x

W¹,¹ Poincaré on an arbitrary Euclidean ball, with the volume-scaled constant.