Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Euclidean.OperatorConstantNonneg

Operator Constant Nonneg #

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

source
theorem CKN.Foundation.Euclidean.czGradientOperatorConstant_nonneg :
0 ≤ czGradientOperatorConstant

The gradient operator constant is nonnegative.

source
theorem CKN.Foundation.Euclidean.czP1OperatorConstant_nonneg :
0 ≤ czP1OperatorConstant

The P1 operator constant is nonnegative.

source
theorem CKN.lin34ForceConstant_nonneg {C₁₃ : ℝ} (hC : 0 ≤ C₁₃) :
0 ≤ lin34ForceConstant C₁₃

The Lin 3.4 force constant is nonnegative given a nonnegative parameter.