Local div–curl estimate for smooth fields

For a smooth vector field on a ball, the square integral of its gradient on a smaller ball is controlled by the square integrals of its divergence, of its antisymmetric derivative and of the field itself on the larger ball (the smooth case of lem:local-div-curl of the Escauriaza–Seregin–Šverák manuscript). For a compactly supported smooth field the gradient identity ∫ |∇W|² = ∫ (div W)² + ½ ∫ Σ (∂ₐW_b - ∂_bWₐ)² follows from two integrations by parts; a cutoff localizes it.

theorem CKN.vorticityDivCurlSmooth_deriv_comm {f : Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (a b : Fin 3) (x : Foundation.Parabolic.Vec3) : spatialDeriv (spatialDeriv f b) a x = spatialDeriv (spatialDeriv f a) b x

Mixed coordinate derivatives of a smooth function on space commute.

theorem CKN.vorticityDivCurlSmooth_integrable {K : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) {F : Foundation.Parabolic.Vec3 → ℝ} (hF : Continuous F) (h0 : ∀ x ∉ K, F x = 0) : MeasureTheory.Integrable F MeasureTheory.volume

A continuous function vanishing off a compact set is integrable.

theorem CKN.vorticityDivCurlSmooth_cross {W : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hW : ∀ (b : Fin 3), ContDiff ℝ (↑⊤) (W b)) (hWc : ∀ (b : Fin 3), HasCompactSupport (W b)) (a b : Fin 3) : ∫ (x : Foundation.Parabolic.Vec3), spatialDeriv (W b) a x * spatialDeriv (W a) b x = ∫ (x : Foundation.Parabolic.Vec3), spatialDeriv (W a) a x * spatialDeriv (W b) b x

Symmetry of the cross terms after two integrations by parts.

theorem CKN.vorticityDivCurlSmooth_integral_le {W : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hW : ∀ (b : Fin 3), ContDiff ℝ (↑⊤) (W b)) (hWc : ∀ (b : Fin 3), HasCompactSupport (W b)) : ∫ (x : Foundation.Parabolic.Vec3), ∑ a : Fin 3, ∑ b : Fin 3, spatialDeriv (W b) a x ^ 2 ≤ ∫ (x : Foundation.Parabolic.Vec3), (∑ a : Fin 3, spatialDeriv (W a) a x) ^ 2 + ∑ a : Fin 3, ∑ b : Fin 3, (spatialDeriv (W b) a x - spatialDeriv (W a) b x) ^ 2

The gradient identity for compactly supported smooth fields, in inequality form.

theorem CKN.vorticityDivCurlSmooth_sq_add_le (x y : ℝ) : (x + y) ^ 2 ≤ 2 * x ^ 2 + 2 * y ^ 2

Two-term squares.

theorem CKN.vorticityDivCurlSmooth_sum_sq_le (f : Fin 3 → ℝ) : (∑ a : Fin 3, f a) ^ 2 ≤ 3 * ∑ a : Fin 3, f a ^ 2

Three-term sums of squares.

theorem CKN.vorticityDivCurlSmooth_mul_sq_le {d v L : ℝ} (hd : |d| ≤ L) : (d * v) ^ 2 ≤ L ^ 2 * v ^ 2

A bounded factor.

theorem CKN.vorticityDivCurlSmooth_pointwise {p L : ℝ} (d v : Fin 3 → ℝ) (g : Fin 3 → Fin 3 → ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hd : ∀ (a : Fin 3), |d a| ≤ L) : (∑ a : Fin 3, (d a * v a + p * g a a)) ^ 2 + ∑ a : Fin 3, ∑ b : Fin 3, (d a * v b + p * g a b - (d b * v a + p * g b a)) ^ 2 ≤ (2 + 30 * L ^ 2) * ((∑ a : Fin 3, g a a) ^ 2 + ∑ a : Fin 3, ∑ b : Fin 3, (g a b - g b a) ^ 2 + ∑ b : Fin 3, v b ^ 2)

The pointwise algebra behind the cutoff step.

theorem CKN.vorticityDivCurlSmooth_local {r R : ℝ} (hr : 0 < r) (hrR : r < R) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x₀ : Foundation.Parabolic.Vec3) (V : Fin 3 → Foundation.Parabolic.Vec3 → ℝ), (∀ (b : Fin 3), ContDiff ℝ (↑⊤) (V b)) → ∫ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, ∑ a : Fin 3, ∑ b : Fin 3, spatialDeriv (V b) a x ^ 2 ≤ C * ∫ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ R, (∑ a : Fin 3, spatialDeriv (V a) a x) ^ 2 + ∑ a : Fin 3, ∑ b : Fin 3, (spatialDeriv (V b) a x - spatialDeriv (V a) b x) ^ 2 + ∑ b : Fin 3, V b x ^ 2

Local div–curl estimate for smooth fields (smooth case of lem:local-div-curl (ESS)).