Ext Sobolev Ball Supported

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

theorem CKN.extSobolevBall_unitBall (x₀ : Foundation.Parabolic.Vec3) (v : H1Function (euclideanBall x₀ 1)) : lpNormOn 6 (euclideanBall x₀ 1) v.toFun ≤ ENNReal.ofReal sobolevPoincareFaithfulC5 * (weakGradientLpNormOn 2 (euclideanBall x₀ 1) v.grad + lpNormOn 2 (euclideanBall x₀ 1) v.toFun)

The absolute-constant unit-ball instance of external Sobolev embedding clause (ii), with the repository's representative-level H¹ norm.

theorem CKN.extSobolevBall_everyBall {x₀ : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) (v : H1Function (euclideanBall x₀ r)) : lpNormOn 6 (euclideanBall x₀ r) v.toFun ≤ ENNReal.ofReal sobolevPoincareFaithfulC5 * (weakGradientLpNormOn 2 (euclideanBall x₀ r) v.grad + (ENNReal.ofReal r)⁻¹ * lpNormOn 2 (euclideanBall x₀ r) v.toFun)

The scale-explicit H¹ → L⁶ estimate on every Euclidean ball, with the same absolute constant as the faithful ball Sobolev–Poincaré result.

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

The spatial q = 10/3 interpolation inequality on every Euclidean ball; this is the integrand estimate used for the ball case of clause (iv).

theorem CKN.extSobolevBall_timeTenThirds {x₀ : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) {J : Set ℝ} {u : ℝ → H1Function (euclideanBall x₀ r)} {A G : ENNReal} (hA : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, lpNormOn 2 (euclideanBall x₀ r) (u t).toFun ≤ A) (hgrad : AEMeasurable (fun (t : ℝ) => weakGradientLpNormOn 2 (euclideanBall x₀ r) (u t).grad ^ 2) (MeasureTheory.volume.restrict J)) (hG : ∫⁻ (t : ℝ) in J, weakGradientLpNormOn 2 (euclideanBall x₀ r) (u t).grad ^ 2 ≤ G) : ∃ (C₆ : ENNReal), C₆ ≠ ⊤ ∧ ∫⁻ (t : ℝ) in J, lpNormOn (ENNReal.ofReal (10 / 3)) (euclideanBall x₀ r) (u t).toFun ^ (10 / 3) ≤ C₆ * A ^ (4 / 3) * G + C₆ * ENNReal.ofReal r ^ (-2) * A ^ (10 / 3) * MeasureTheory.volume J

Time integration of the same-ball q = 10/3 inequality. hA is the essential L∞_t L²_x bound and hG is the integrated squared spatial-gradient bound.

theorem CKN.extSobolevBall_productIntegral_eq_timeSlices {x₀ : Foundation.Parabolic.Vec3} {r : ℝ} {J : Set ℝ} {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {u : ℝ → H1Function (euclideanBall x₀ r)} (hF : AEMeasurable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => ‖g z‖ₑ ^ (10 / 3)) ((MeasureTheory.volume.restrict (euclideanBall x₀ r)).prod (MeasureTheory.volume.restrict J))) (hrep : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict (euclideanBall x₀ r), g (x, s) = (u s).toFun x) : ∫⁻ (z : Vec 3 × ℝ) in euclideanBall x₀ r ×ˢ J, ‖g z‖ₑ ^ (10 / 3) = ∫⁻ (s : ℝ) in J, lpNormOn (ENNReal.ofReal (10 / 3)) (euclideanBall x₀ r) (u s).toFun ^ (10 / 3)

Identify the product-space L^(10/3) integral with the time integral of the H¹ slice norms when the measurable space-time representative agrees with those slices almost everywhere.

theorem CKN.extSobolevBall_productTenThirds {x₀ : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) {J : Set ℝ} {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {u : ℝ → H1Function (euclideanBall x₀ r)} {A : ENNReal} (hA : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, lpNormOn 2 (euclideanBall x₀ r) (u t).toFun ≤ A) (hgrad : AEMeasurable (fun (t : ℝ) => weakGradientLpNormOn 2 (euclideanBall x₀ r) (u t).grad ^ 2) (MeasureTheory.volume.restrict J)) (hF : AEMeasurable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => ‖g z‖ₑ ^ (10 / 3)) ((MeasureTheory.volume.restrict (euclideanBall x₀ r)).prod (MeasureTheory.volume.restrict J))) (hrep : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict (euclideanBall x₀ r), g (x, s) = (u s).toFun x) : ∃ (C₆ : ENNReal), C₆ ≠ ⊤ ∧ ∫⁻ (z : Vec 3 × ℝ) in euclideanBall x₀ r ×ˢ J, ‖g z‖ₑ ^ (10 / 3) ≤ (C₆ * A ^ (4 / 3) * ∫⁻ (t : ℝ) in J, weakGradientLpNormOn 2 (euclideanBall x₀ r) (u t).grad ^ 2) + C₆ * ENNReal.ofReal r ^ (-2) * A ^ (10 / 3) * MeasureTheory.volume J

Product-space ball form of the parabolic L^(10/3) estimate.