Interpolation Ball

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

noncomputable def CKN.interpolationTheta (q : ℝ) : ℝ

Interpolation weight relating the velocity exponent to the L² and L⁶ endpoints.

Equations

• CKN.interpolationTheta q = 3 * (q - 2) / (2 * q)

noncomputable def CKN.interpolationExponent (q : ℝ) : ℝ

Exponent of the gradient contribution in the velocity interpolation estimate.

Equations

• CKN.interpolationExponent q = 3 * (q - 2) / 4

theorem CKN.interpolationBall_of_sobolev (hsob : ∃ (S : ENNReal), ∀ {x₀ : Vec 3} {r : ℝ}, 0 < r → ∀ (v : H1Function (euclideanBall x₀ r)), lpNormOn 6 (euclideanBall x₀ r) v.toFun ≤ S * (weakGradientLpNormOn 2 (euclideanBall x₀ r) v.grad + (ENNReal.ofReal r)⁻¹ * lpNormOn 2 (euclideanBall x₀ r) v.toFun)) : ∃ (C₆ : ENNReal), ∀ (q : ℝ), 2 ≤ q → q ≤ 6 → ∀ {x₀ : Vec 3} {r : ℝ}, 0 < r → ∀ (v : H1Function (euclideanBall x₀ r)), lpNormOn (ENNReal.ofReal q) (euclideanBall x₀ r) v.toFun ^ q ≤ C₆ * weakGradientLpNormOn 2 (euclideanBall x₀ r) v.grad ^ (2 * interpolationExponent q) * lpNormOn 2 (euclideanBall x₀ r) v.toFun ^ (q - 2 * interpolationExponent q) + C₆ * ENNReal.ofReal r ^ (-(2 * interpolationExponent q)) * lpNormOn 2 (euclideanBall x₀ r) v.toFun ^ q

theorem CKN.interpolationBall : ∃ (C₆ : ENNReal), ∀ (q : ℝ), 2 ≤ q → q ≤ 6 → ∀ {x₀ : Vec 3} {r : ℝ}, 0 < r → ∀ (v : H1Function (euclideanBall x₀ r)), lpNormOn (ENNReal.ofReal q) (euclideanBall x₀ r) v.toFun ^ q ≤ C₆ * weakGradientLpNormOn 2 (euclideanBall x₀ r) v.grad ^ (2 * interpolationExponent q) * lpNormOn 2 (euclideanBall x₀ r) v.toFun ^ (q - 2 * interpolationExponent q) + C₆ * ENNReal.ofReal r ^ (-(2 * interpolationExponent q)) * lpNormOn 2 (euclideanBall x₀ r) v.toFun ^ q

The interpolation estimate on every positive-radius Euclidean ball. This statement does not record finiteness of its ℝ≥0∞ coefficient; use interpolationBall_finite for the finite-constant estimate, or interpolationBall_three_finite for its cubic specialization.

The witness supplied by the Sobolev bridge is finite. Keeping this fact separate lets cylinder arguments pass from ℝ≥0∞ estimates to the real scale quantities without introducing an artificial finiteness hypothesis.

theorem CKN.interpolationBall_finite : ∃ (C₆ : ENNReal), C₆ ≠ ⊤ ∧ ∀ (q : ℝ), 2 ≤ q → q ≤ 6 → ∀ {x₀ : Vec 3} {r : ℝ}, 0 < r → ∀ (v : H1Function (euclideanBall x₀ r)), lpNormOn (ENNReal.ofReal q) (euclideanBall x₀ r) v.toFun ^ q ≤ C₆ * weakGradientLpNormOn 2 (euclideanBall x₀ r) v.grad ^ (2 * interpolationExponent q) * lpNormOn 2 (euclideanBall x₀ r) v.toFun ^ (q - 2 * interpolationExponent q) + C₆ * ENNReal.ofReal r ^ (-(2 * interpolationExponent q)) * lpNormOn 2 (euclideanBall x₀ r) v.toFun ^ q

A finite constant witnesses the interpolation estimate on every ball.

theorem CKN.interpolationBall_three_finite : ∃ (C₆ : ENNReal), C₆ ≠ ⊤ ∧ ∀ {x₀ : Vec 3} {r : ℝ}, 0 < r → ∀ (v : H1Function (euclideanBall x₀ r)), lpNormOn 3 (euclideanBall x₀ r) v.toFun ^ 3 ≤ C₆ * weakGradientLpNormOn 2 (euclideanBall x₀ r) v.grad ^ (3 / 2) * lpNormOn 2 (euclideanBall x₀ r) v.toFun ^ (3 / 2) + C₆ * ENNReal.ofReal r ^ (-(3 / 2)) * lpNormOn 2 (euclideanBall x₀ r) v.toFun ^ 3

The finite-witness interpolation estimate specialized to the cubic slice exponent used on parabolic cylinders.