Unit-ball Sobolev localization through the two-reflection extension

The compactly supported cutoff of the C¹ extension is the smooth input for the same-ball estimate. This module records the localization step explicitly; the remaining reduction of its outer-ball terms to the original ball is kept separate.

theorem CKN.seeleyCutoffExtension_contDiff (v : Vec 3 → ℝ) (hv : ContDiff ℝ 1 v) : ContDiff ℝ 1 (seeleyCutoffExtension v)

theorem CKN.seeleyCutoffExtension_eq_on_unitBall {v : Vec 3 → ℝ} {x : Vec 3} (hx : x ∈ euclideanBall 0 1) : seeleyCutoffExtension v x = v x

theorem CKN.seeleyLocalizedSobolevBound (v : Vec 3 → ℝ) (c : ℝ) (hv : ContDiff ℝ 1 v) : (lpNormOn 6 (euclideanBall 0 1) fun (x : Vec 3) => v x - c) ≤ localSobolevConstant * (gradientLpNormOn 2 (euclideanBall 0 2) (seeleyCutoffExtension fun (x : Vec 3) => v x - c) + ↑(Real.toNNReal 32) * lpNormOn 2 (euclideanBall 0 2) (seeleyCutoffExtension fun (x : Vec 3) => v x - c))

noncomputable def CKN.sobolevPoincareL6Constant : ENNReal

Finite coefficient in the L⁶ Poincare–Sobolev estimate on a Euclidean ball.

Equations

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

theorem CKN.sobolevPoincare_L6_unit (v : Vec 3 → ℝ) (hv : ContDiff ℝ 1 v) : (lpNormOn 6 (euclideanBall 0 1) fun (x : Vec 3) => v x - MeasureTheory.average (MeasureTheory.volume.restrict (euclideanBall 0 1)) v) ≤ sobolevPoincareL6Constant * gradientLpNormOn 2 (euclideanBall 0 1) v

theorem CKN.sobolevPoincare_L6_ball (x₀ : Vec 3) {r : ℝ} (hr : 0 < r) (v : Vec 3 → ℝ) (hv : ContDiff ℝ 1 v) : (lpNormOn 6 (euclideanBall x₀ r) fun (x : Vec 3) => v x - MeasureTheory.average (MeasureTheory.volume.restrict (euclideanBall x₀ r)) v) ≤ sobolevPoincareL6Constant * gradientLpNormOn 2 (euclideanBall x₀ r) v