Smooth Sobolev inequalities on three-dimensional space

The whole-space estimates used in lem:vorticity-products of the Escauriaza–Seregin–Šverák manuscript.

theorem CKN.gradL4_sq_le_smooth_scalar (f : Foundation.Parabolic.Vec3 → ℝ) (M : ℝ) (hf : ContDiff ℝ (↑⊤) f) (hfc : HasCompactSupport f) (hM : ∀ (x : Foundation.Parabolic.Vec3), |f x| ≤ M) : MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => (∑ j : Fin 3, spatialDeriv f j x ^ 2) ^ 2) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => ∑ j : Fin 3, ∑ k : Fin 3, spatialDeriv (spatialDeriv f j) k x ^ 2) MeasureTheory.volume ∧ ∫ (x : Foundation.Parabolic.Vec3), (∑ j : Fin 3, spatialDeriv f j x ^ 2) ^ 2 ≤ 28 * M ^ 2 * ∫ (x : Foundation.Parabolic.Vec3), ∑ j : Fin 3, ∑ k : Fin 3, spatialDeriv (spatialDeriv f j) k x ^ 2

A scalar whole-space Gagliardo–Nirenberg estimate for smooth compactly supported functions.

theorem CKN.abs_le_sobolevTwo_smooth : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) f → HasCompactSupport f → ∀ (x : Foundation.Parabolic.Vec3), |f x| ≤ C * √(sobolevNormSqOn 2 Set.univ fun (α : List (Fin 3)) => wordDeriv α f)

The order-two Sobolev norm controls every value of a smooth compactly supported function in three dimensions (lem:vorticity-products, ESS).