The ball Poincare inequality for representative-level W^{1,p} functions

The proof uses interior mollification on compactly contained balls and then exhausts the original ball.

theorem CKN.opNorm_eq_sum_abs_basis (L : Vec 3 →L[ℝ] ℝ) : ‖L‖ = ∑ i : Fin 3, |L (basisVec i)|

def CKN.w1pGradientNorm {U : Set (Vec 3)} {p : ENNReal} (u : W1pFunction U p) : Vec 3 → ℝ

The native coordinate-gradient norm used by the scalar W^{1,p} result.

Equations

• CKN.w1pGradientNorm u x = ∑ i : Fin 3, |u.grad x i|