The same-ball W^{1,1} to L^{3/2} estimate

The endpoint estimate is obtained by subtracting the ball average, applying the two-reflection extension and a compact cutoff, and then using the global Gagliardo--Nirenberg inequality at p = 1. The affine bookkeeping is kept explicit so that the final constant is independent of the ball.

def CKN.unitEuclideanBall : Set (Vec 3)

Unit Euclidean ball used for the L¹ Poincare–Sobolev inequality.

Equations

• CKN.unitEuclideanBall = CKN.euclideanBall 0 1

theorem CKN.unitEuclideanBall_bounded : IsBoundedDomain unitEuclideanBall

noncomputable def CKN.unitL1PoincareConstant : ℝ

Explicit L¹ Poincare coefficient on the unit Euclidean ball.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.poincareSobolevL1Constant : ENNReal

The absolute unit-ball constant in the smooth W^{1,1} endpoint estimate.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.poincareSobolevL1_unit (g : Vec 3 → ℝ) (hg : ContDiff ℝ 1 g) : MeasureTheory.eLpNorm (fun (x : Vec 3) => g x - integralAverage (euclideanBall 0 1) g) (↑(3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 1)) ≤ poincareSobolevL1Constant * MeasureTheory.eLpNorm (fderiv ℝ g) 1 (MeasureTheory.volume.restrict (euclideanBall 0 1))

Unit-ball W^{1,1} to L^{3/2} Poincare--Sobolev estimate for C¹ functions.

The left side is the extended L^{3/2} seminorm of the function after subtracting its ball average; the right side is the L¹ seminorm of its Fréchet derivative.