Seeley Poincare

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

def CKN.seeleyUnitEuclideanBall : Set (Vec 3)

Unit Euclidean ball used as the reference domain for the Seeley construction.

Equations

• CKN.seeleyUnitEuclideanBall = CKN.euclideanBall 0 1

theorem CKN.seeleyUnitEuclideanBall_domain : IsOpenBoundedConvexDomain seeleyUnitEuclideanBall

theorem CKN.euclideanClosedBall_one_ae_eq_euclideanBall : euclideanClosedBall 0 1 =ᵐ[MeasureTheory.volume] euclideanBall 0 1

noncomputable def CKN.euclideanBallPoincareConstant : ENNReal

Explicit L² Poincare coefficient on the unit Euclidean ball.

Equations

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

theorem CKN.euclideanBall_value_energy_poincare (v : Vec 3 → ℝ) (hv : ContDiff ℝ 1 v) : ∫⁻ (x : Vec 3) in euclideanBall 0 1, ENNReal.ofReal |v x - MeasureTheory.average (MeasureTheory.volume.restrict (euclideanBall 0 1)) v| ^ 2 ≤ euclideanBallPoincareConstant * ∫⁻ (y : Vec 3) in euclideanBall 0 1, ENNReal.ofReal (‖classicalGradient v y‖ ^ 2)