Local Sobolev and interpolation inequalities for smooth functions

This file proves local Sobolev and interpolation inequalities for smooth functions. The corresponding weak H¹ estimate has the form

‖u‖₆(Bᵣ) ≤ C (‖∇u‖₂(B₂ᵣ) + r⁻¹ ‖u‖₂(B₂ᵣ)).

Passing from smooth functions to weak H¹ functions requires local approximation of both the function and its gradient, together with the weak product rule for a smooth cutoff. Interpolation yields the L³ and L^(10/3) estimates; for Q_r = (t-r²,t) × B_r, the L³ cylinder factor is r^(1/2).

noncomputable def CKN.lpNormOn (p : ENNReal) (s : Set (Vec 3)) (u : Vec 3 → ℝ) : ENNReal

The extended Lᵖ seminorm of a function on a measurable set.

Equations

• CKN.lpNormOn p s u = MeasureTheory.eLpNorm u p (MeasureTheory.volume.restrict s)

noncomputable def CKN.gradientLpNormOn (p : ENNReal) (s : Set (Vec 3)) (u : Vec 3 → ℝ) : ENNReal

The extended Lᵖ seminorm of the native classical gradient.

Equations

• CKN.gradientLpNormOn p s u = MeasureTheory.eLpNorm (CKN.classicalGradient u) p (MeasureTheory.volume.restrict s)

theorem CKN.fderiv_norm_le_three_classicalGradient {f : Vec 3 → ℝ} (x : Vec 3) : ‖fderiv ℝ f x‖ ≤ 3 * ‖classicalGradient f x‖

noncomputable def CKN.localSobolevConstant : ENNReal

Euclidean Sobolev coefficient inherited from Mathlib's compact-support inequality.

Equations

• CKN.localSobolevConstant = ↑3 * ↑(MeasureTheory.SNormLESNormFDerivOfEqConst ℝ MeasureTheory.volume 2)

theorem CKN.smoothSobolevBall {x₀ : Vec 3} {r : ℝ} (hr : 0 < r) {u : Vec 3 → ℝ} (hu : ContDiff ℝ 1 u) : lpNormOn 6 (euclideanBall x₀ r) u ≤ localSobolevConstant * (gradientLpNormOn 2 (euclideanBall x₀ (2 * r)) u + ↑(32 / r).toNNReal * lpNormOn 2 (euclideanBall x₀ (2 * r)) u)