Approximation lemmas for Sobolev–Poincaré on Euclidean balls

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

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

Local W¹,¹ Poincaré on a compactly contained Euclidean ball.

theorem CKN.sum_abs_le_sqrt_three_vec3EuclideanNormFaithful (v : Foundation.Parabolic.Vec3) : ∑ i : Fin 3, |v i| ≤ √3 * Foundation.Parabolic.vec3EuclideanNorm v

The coordinatewise gradient sum is controlled by the Euclidean norm in dimension three.