The scale-explicit Sobolev–Poincaré inequalities on Euclidean balls

This file records the three clauses of the ball lemma together with one constant chosen independently of the ball and the functions.

noncomputable def CKN.sobolevPoincareFaithfulC5 : ℝ

A single absolute constant for all three clauses of the ball lemma.

Equations

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

theorem CKN.sobolevPoincareL6Constant_nonneg : 0 ≤ sobolevPoincareL6Constant.toReal

The constant in the existing mean-zero L⁶ estimate is nonnegative.

theorem CKN.sobolevPoincareL6Constant_pos_faithful : 0 < sobolevPoincareL6Constant

The chosen mean-zero Sobolev constant is nonzero, by the bump-function lower bound.

theorem CKN.sobolevPoincareFaithfulC5_pos : 0 < sobolevPoincareFaithfulC5

C₅ is positive.

theorem CKN.sobolevPoincare_ball_L1_faithful (x₀ : Foundation.Parabolic.Vec3) {r : ℝ} (hr : 0 < r) (u : W1pFunction (euclideanBall x₀ r) 1) : ∫ (x : Vec 3) in euclideanBall x₀ r, |u.toFun x - MeasureTheory.average (MeasureTheory.volume.restrict (euclideanBall x₀ r)) u.toFun| ≤ sobolevPoincareFaithfulC5 * r * ∫ (x : Vec 3) in euclideanBall x₀ r, Foundation.Parabolic.vec3EuclideanNorm (u.grad x)

The full scale-explicit (L^1) Poincaré clause on every Euclidean ball.

theorem CKN.sobolevPoincare_ball_L6_faithful (x₀ : Foundation.Parabolic.Vec3) {r : ℝ} (hr : 0 < r) : (∀ (v : H1Function (euclideanBall x₀ r)), (lpNormOn 6 (Foundation.Parabolic.vec3Ball x₀ r) fun (x : Vec 3) => v.toFun x - MeasureTheory.average (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ r)) v.toFun) ≤ ENNReal.ofReal sobolevPoincareFaithfulC5 * weakGradientLpNormOn 2 (Foundation.Parabolic.vec3Ball x₀ r) v.grad) ∧ ∀ (v : H1Function (euclideanBall x₀ r)), lpNormOn 6 (Foundation.Parabolic.vec3Ball x₀ r) v.toFun ≤ ENNReal.ofReal sobolevPoincareFaithfulC5 * (weakGradientLpNormOn 2 (Foundation.Parabolic.vec3Ball x₀ r) v.grad + (ENNReal.ofReal r)⁻¹ * lpNormOn 2 (Foundation.Parabolic.vec3Ball x₀ r) v.toFun)

The mean-zero and full L⁶ clauses of Sobolev–Poincaré on every Euclidean ball.

theorem CKN.sobolevPoincare_ball_faithful (x₀ : Foundation.Parabolic.Vec3) {r : ℝ} (hr : 0 < r) : (∀ (v : H1Function (euclideanBall x₀ r)), (lpNormOn 6 (Foundation.Parabolic.vec3Ball x₀ r) fun (x : Vec 3) => v.toFun x - MeasureTheory.average (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ r)) v.toFun) ≤ ENNReal.ofReal sobolevPoincareFaithfulC5 * weakGradientLpNormOn 2 (Foundation.Parabolic.vec3Ball x₀ r) v.grad) ∧ (∀ (v : H1Function (euclideanBall x₀ r)), lpNormOn 6 (Foundation.Parabolic.vec3Ball x₀ r) v.toFun ≤ ENNReal.ofReal sobolevPoincareFaithfulC5 * (weakGradientLpNormOn 2 (Foundation.Parabolic.vec3Ball x₀ r) v.grad + (ENNReal.ofReal r)⁻¹ * lpNormOn 2 (Foundation.Parabolic.vec3Ball x₀ r) v.toFun)) ∧ ∀ (u : W1pFunction (euclideanBall x₀ r) 1), ∫ (x : Vec 3) in euclideanBall x₀ r, |u.toFun x - MeasureTheory.average (MeasureTheory.volume.restrict (euclideanBall x₀ r)) u.toFun| ≤ sobolevPoincareFaithfulC5 * r * ∫ (x : Vec 3) in euclideanBall x₀ r, Foundation.Parabolic.vec3EuclideanNorm (u.grad x)

The three scale-explicit clauses of the paper's ball lemma, with one constant chosen uniformly in the centre, radius, and function.