Sobolev Poincare Constant Pos

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.sNormLESNormFDerivOfEqConst_vec3_two_pos : 0 < MeasureTheory.SNormLESNormFDerivOfEqConst ℝ MeasureTheory.volume 2

The Sobolev inequality constant SNormLESNormFDerivOfEqConst for E := Vec 3, F := ℝ, μ := volume, and p := 2 is positive.

theorem CKN.localSobolevConstant_pos : 0 < localSobolevConstant

localSobolevConstant is positive.

theorem CKN.sobolevPoincareL6Constant_pos : 0 < sobolevPoincareL6Constant

sobolevPoincareL6Constant is positive.