Sobolev Poincare Constant Finite

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

theorem CKN.localSobolevConstant_ne_top : localSobolevConstant ≠ ⊤

The local Sobolev constant is finite.

theorem CKN.euclideanBallPoincareConstant_ne_top : euclideanBallPoincareConstant ≠ ⊤

The Euclidean ball Poincaré constant is finite.

theorem CKN.sobolevPoincareL6Constant_ne_top : sobolevPoincareL6Constant ≠ ⊤

The Sobolev–Poincaré L⁶ constant is finite.

theorem CKN.sobolevPoincareL6Constant_lt_top : sobolevPoincareL6Constant < ⊤

The Sobolev–Poincaré L⁶ constant is less than ∞.

theorem CKN.ofReal_toReal_sobolevPoincareL6Constant : ENNReal.ofReal sobolevPoincareL6Constant.toReal = sobolevPoincareL6Constant

sobolevPoincareL6Constant is real: ENNReal.ofReal of its toReal equals itself.