The rescaled L¹ Poincaré display

The scale-invariant L^{3/2} Poincaré inequality gives the L¹ display after Hölder on the ball and comparison of the differential norm with the Euclidean norm of the gradient. These steps contribute respectively (4π/3)^(1/3) r and √3 to the constant.

theorem CKN.poincareSobolevL1_ball_of_unit {x₀ : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) (g : Foundation.Parabolic.Vec3 → ℝ) (hg : ContDiff ℝ 1 g) : ∫ (x : Vec 3) in euclideanBall x₀ r, |g x - ⨍ (y : Vec 3) in euclideanBall x₀ r, g y| ≤ (Real.pi * 4 / 3) ^ (1 / 3) * √3 * poincareSobolevL1Constant.toReal * r * ∫ (x : Vec 3) in euclideanBall x₀ r, Foundation.Parabolic.vec3EuclideanNorm (classicalGradient g x)

The rescaled L¹ Poincaré display on every Euclidean ball, with the correct absolute constant (4π/3)^(1/3) √3 · poincareSobolevL1Constant.toReal.