A local sup bound for smooth functions by second derivatives

For a smooth function on space, the value at every point of a closed ball is controlled by the L² norms of the function and of its first and second coordinate derivatives on a larger open ball. This is the three-dimensional embedding of order two used for the pointwise bounds of thm:vorticity-regularity of the Escauriaza–Seregin–Šverák manuscript: a cutoff reduces it to the whole-space estimate CKN.smooth_global_linf_uniform, and the first derivatives of the cutoff product are placed in L⁶ by CKN.sobolev_L6_global.

theorem CKN.vorticitySobolevSmooth_eLpNorm_le {E : Type u_1} [NormedAddCommGroup E] {h : Foundation.Parabolic.Vec3 → E} (hh : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume) {B : Foundation.Parabolic.Vec3 → ℝ} (hB : MeasureTheory.Integrable B MeasureTheory.volume) (hpt : ∀ (y : Foundation.Parabolic.Vec3), ‖h y‖ ^ 2 ≤ B y) : MeasureTheory.eLpNorm h 2 MeasureTheory.volume ≤ ENNReal.ofReal √(∫ (y : Foundation.Parabolic.Vec3), B y)

An L² bound from a pointwise bound of the square by an integrable function.

theorem CKN.vorticitySobolevSmooth_lpNorm_le {E : Type u_1} [NormedAddCommGroup E] {h : Foundation.Parabolic.Vec3 → E} (hh : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume) {B : Foundation.Parabolic.Vec3 → ℝ} (hB : MeasureTheory.Integrable B MeasureTheory.volume) (hpt : ∀ (y : Foundation.Parabolic.Vec3), ‖h y‖ ^ 2 ≤ B y) : MeasureTheory.lpNorm h 2 MeasureTheory.volume ≤ √(∫ (y : Foundation.Parabolic.Vec3), B y)

The real L² norm version of CKN.vorticitySobolevSmooth_eLpNorm_le.

theorem CKN.vorticitySobolevSmooth_four_sq {a b c d p q s t M : ℝ} (ha : |a| ≤ M) (hb : |b| ≤ M) (hc : |c| ≤ M) (hd : |d| ≤ M) : (a * p + b * q + c * s + d * t) ^ 2 ≤ 4 * M ^ 2 * (p ^ 2 + q ^ 2 + s ^ 2 + t ^ 2)

The elementary square bound for four products with bounded first factors.

theorem CKN.vorticitySobolevSmooth_sup {r R : ℝ} (hr : 0 < r) (hrR : r < R) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x₀ : Foundation.Parabolic.Vec3) (f : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) f → ∀ (x : Foundation.Parabolic.Vec3), Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ≤ r → |f x| ^ 2 ≤ C * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ R, f y ^ 2 + ∑ j : Fin 3, spatialDeriv f j y ^ 2 + ∑ j : Fin 3, ∑ k : Fin 3, spatialDeriv (spatialDeriv f j) k y ^ 2

Local sup bound of order two: the value of a smooth function at a point of the closed ball of radius r is controlled by the L² norms of the function and of its first and second coordinate derivatives on the open ball of radius R (the pointwise embedding used in thm:vorticity-regularity (ESS)).