Local Sobolev and interpolation inequalities for H¹ representatives

The proof first multiplies the representative by the canonical compactly supported cutoff inside the outer ball. The product rule gives a global weak gradient for this zero extension; global mollification then supplies smooth functions, and Fatou's lemma passes the estimate to the representative. This preserves the absolute constant from the smooth estimate.

noncomputable def CKN.weakGradientLpNormOn (p : ENNReal) (s : Set (Vec 3)) (Du : Vec 3 → Vec 3) : ENNReal

The extended Lᵖ seminorm of a chosen weak gradient on a set.

Equations

• CKN.weakGradientLpNormOn p s Du = MeasureTheory.eLpNorm Du p (MeasureTheory.volume.restrict s)

theorem CKN.eLpNorm_pi_le_sum {f : Vec 3 → Vec 3} {μ : MeasureTheory.Measure (Vec 3)} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.eLpNorm f 2 μ ≤ ∑ i : Fin 3, MeasureTheory.eLpNorm (fun (x : Vec 3) => f x i) 2 μ

theorem CKN.h1SobolevBall {x₀ : Vec 3} {r : ℝ} (hr : 0 < r) (u : H1Function (euclideanBall x₀ (2 * r))) : lpNormOn 6 (euclideanBall x₀ r) u.toFun ≤ localSobolevConstant * (weakGradientLpNormOn 2 (euclideanBall x₀ (2 * r)) u.grad + ↑(32 / r).toNNReal * lpNormOn 2 (euclideanBall x₀ (2 * r)) u.toFun)

Local L⁶ Sobolev control for an H¹ representative on concentric balls.

theorem CKN.h1InterpolationBall {x₀ : Vec 3} {r : ℝ} (hr : 0 < r) (u : H1Function (euclideanBall x₀ (2 * r))) : lpNormOn 3 (euclideanBall x₀ r) u.toFun ≤ lpNormOn 2 (euclideanBall x₀ (2 * r)) u.toFun ^ (1 / 2) * (localSobolevConstant * (weakGradientLpNormOn 2 (euclideanBall x₀ (2 * r)) u.grad + ↑(32 / r).toNNReal * lpNormOn 2 (euclideanBall x₀ (2 * r)) u.toFun)) ^ (1 / 2)

Local L³ interpolation control for an H¹ representative on concentric balls.

theorem CKN.h1InterpolationBallCubed {x₀ : Vec 3} {r : ℝ} (hr : 0 < r) (u : H1Function (euclideanBall x₀ (2 * r))) : lpNormOn 3 (euclideanBall x₀ r) u.toFun ^ 3 ≤ localSobolevConstant ^ (3 / 2) * lpNormOn 2 (euclideanBall x₀ (2 * r)) u.toFun ^ (3 / 2) * (weakGradientLpNormOn 2 (euclideanBall x₀ (2 * r)) u.grad + ↑(32 / r).toNNReal * lpNormOn 2 (euclideanBall x₀ (2 * r)) u.toFun) ^ (3 / 2)

Cubed local L³ interpolation control for an H¹ representative.

theorem CKN.h1InterpolationCylinderL3 {x₀ : Vec 3} {r t : ℝ} (hr : 0 < r) {u : ℝ → H1Function (euclideanBall x₀ (2 * r))} : ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, lpNormOn 3 (euclideanBall x₀ r) (u s).toFun ^ 3 ≤ ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, localSobolevConstant ^ (3 / 2) * lpNormOn 2 (euclideanBall x₀ (2 * r)) (u s).toFun ^ (3 / 2) * (weakGradientLpNormOn 2 (euclideanBall x₀ (2 * r)) (u s).grad + ↑(32 / r).toNNReal * lpNormOn 2 (euclideanBall x₀ (2 * r)) (u s).toFun) ^ (3 / 2)

Time-integrated cubed L³ interpolation control for H¹ representatives.