Vector Inequalities

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

Componentwise vector estimates

theorem CKN.vector_h1_interpolation_cylinder_l3_componentwise {x₀ : Foundation.Parabolic.Vec3} {r t : ℝ} (hr : 0 < r) (u : ℝ → Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hu : Fin 3 → ℝ → H1Function (euclideanBall x₀ (2 * r))) (hcomp : ∀ (i : Fin 3) (s : ℝ), (hu i s).toFun = fun (x : Foundation.Parabolic.Vec3) => u s x i) (i : Fin 3) : ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, (lpNormOn 3 (euclideanBall x₀ r) fun (x : Vec 3) => u s x i) ^ 3 ≤ ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, localSobolevConstant ^ (3 / 2) * (lpNormOn 2 (euclideanBall x₀ (2 * r)) fun (x : Vec 3) => u s x i) ^ (3 / 2) * (weakGradientLpNormOn 2 (euclideanBall x₀ (2 * r)) (hu i s).grad + ↑(32 / r).toNNReal * lpNormOn 2 (euclideanBall x₀ (2 * r)) fun (x : Vec 3) => u s x i) ^ (3 / 2)

The time-integrated cubed interpolation estimate applied to each velocity component.

This estimate uses the larger ball of radius 2 * r for the input norms. For finite-constant interpolation on a single ball, see CKN.interpolationBall_finite in CKN.Setting.InterpolationBall.

Scale quantities

theorem CKN.gamma_le_of_scale_normalized_interpolation {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} : IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ {z : Foundation.Parabolic.ParabolicPoint} {r C : ℝ} (hr : 0 < r), closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 (2 * r)) ⊆ spaceTimeSet Ω I → ∀ (hC : 0 ≤ C) (hα : 0 ≤ alpha u z (2 * r)) (hβ : 0 ≤ beta u Du z (2 * r)) (hfinite : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≠ ⊤) (hinterpolation : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≤ ENNReal.ofReal (r ^ 2 * (C * alpha u z (2 * r) ^ (1 / 2) * beta u Du z (2 * r) ^ (1 / 2) + C * alpha u z (2 * r)) ^ 3)), gamma u z r ≤ C * alpha u z (2 * r) ^ (1 / 2) * beta u Du z (2 * r) ^ (1 / 2) + C * alpha u z (2 * r)

Algebraic translation of a scale-normalized cylinder interpolation estimate into the γ, α, and β quantities.

The hypothesis is the vector-valued cylinder estimate produced by the analytic lift. It is stated as a cube of the desired right-hand side, with the input scale quantities evaluated at 2 * r. The single-ball analytic estimate is available as CKN.interpolationBall_three_finite in CKN.Setting.InterpolationBall.