A local Gagliardo–Nirenberg estimate for bounded smooth functions

For a smooth function bounded by M on a ball, the fourth power of its gradient on a smaller ball is controlled by M² times the square integrals of its first and second derivatives on the larger ball. This is the smooth estimate ‖∇v‖₄² ≤ C ‖v‖_∞ ‖∇²v‖₂ behind the first product bound of lem:vorticity-products of the Escauriaza–Seregin–Šverák manuscript. With A = |∇f|² and a cutoff η, one integration by parts gives ∫ η⁴ A² = -Σⱼ ∫ f ∂ⱼ(η⁴ A ∂ⱼ f), and a pointwise Young inequality absorbs three quarters of the left side.

theorem CKN.vorticityGNSmooth_young {c P Q : ℝ} (hP : 0 ≤ P) (hQ : 0 ≤ Q) (hc : c ^ 2 ≤ 4 * P * Q) : c ≤ P + Q

Young's inequality in the form used for absorption.

theorem CKN.vorticityGNSmooth_neg_mul_le {F M T : ℝ} (hF : |F| ≤ M) : -(F * T) ≤ M * |T|

A bounded factor in front of a product.

theorem CKN.vorticityGNSmooth_quadratic_sq_le (g : Fin 3 → ℝ) (H : Fin 3 → Fin 3 → ℝ) : (∑ j : Fin 3, ∑ k : Fin 3, g j * g k * H j k) ^ 2 ≤ (∑ j : Fin 3, g j ^ 2) ^ 2 * ∑ j : Fin 3, ∑ k : Fin 3, H j k ^ 2

The quadratic form of a matrix is controlled by its Frobenius norm.

theorem CKN.vorticityGNSmooth_pointwise {F M η : ℝ} (d g : Fin 3 → ℝ) (H : Fin 3 → Fin 3 → ℝ) (hF : |F| ≤ M) : -(F * ((4 * η ^ 3 * ∑ j : Fin 3, g j ^ 2) * ∑ j : Fin 3, d j * g j + η ^ 4 * (∑ j : Fin 3, ∑ k : Fin 3, 2 * g k * H j k * g j + (∑ j : Fin 3, g j ^ 2) * ∑ j : Fin 3, H j j))) ≤ 3 / 4 * (η ^ 4 * (∑ j : Fin 3, g j ^ 2) ^ 2) + M ^ 2 * ((16 * η ^ 2 * ∑ j : Fin 3, d j ^ 2) * ∑ j : Fin 3, g j ^ 2 + 7 * η ^ 4 * ∑ j : Fin 3, ∑ k : Fin 3, H k j ^ 2)

The pointwise inequality behind the absorption argument.

theorem CKN.vorticityGNSmooth_deriv_sq {g : Foundation.Parabolic.Vec3 → ℝ} {x : Foundation.Parabolic.Vec3} (hg : DifferentiableAt ℝ g x) (j : Fin 3) : spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => g y ^ 2) j x = 2 * g x * spatialDeriv g j x

Coordinate derivative of a square.

theorem CKN.vorticityGNSmooth_deriv_sum_sq {g : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hg : ∀ (k : Fin 3), Differentiable ℝ (g k)) (j : Fin 3) (x : Foundation.Parabolic.Vec3) : spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => ∑ k : Fin 3, g k y ^ 2) j x = ∑ k : Fin 3, 2 * g k x * spatialDeriv (g k) j x

Coordinate derivative of a sum of three squares.

theorem CKN.vorticityGNSmooth_deriv_pow_four {η : Foundation.Parabolic.Vec3 → ℝ} {x : Foundation.Parabolic.Vec3} (hη : Differentiable ℝ η) (j : Fin 3) : spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => η y ^ 4) j x = 4 * η x ^ 3 * spatialDeriv η j x

Coordinate derivative of a fourth power.

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

Local Gagliardo–Nirenberg estimate for smooth functions bounded on a ball (lem:vorticity-products, ESS).