Lin34 Centred Correction

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

Centring the nonlinearity against the Hessian of a test function

The paper's nonlinearity is introduced in singly centred form U_ij = -u_i (u_j - c_j) and then rewritten in the doubly centred form Û_ij = -(u_i - c_i)(u_j - c_j) of eq:Uhat. The difference between the two tensors is U_ij - Û_ij = -c_i (u_j - c_j), and the point of the present file is that this difference pairs to zero against the Hessian of every smooth compactly supported test function. This is purely a calculus fact: the Hessian of a test function is a divergence, so its pairing with a constant vector field vanishes, and its pairing with the weakly divergence-free field u vanishes by hypothesis.

The file records the two elementary integration-by-parts facts (the integral of a spatial derivative, and of a mixed second derivative, of a compactly supported smooth function) and then assembles the cancellation for the centred pairing.

theorem CKN.lin34_integral_spatialDeriv_eq_zero {G : Foundation.Parabolic.Vec3 → ℝ} (hG : ContDiff ℝ (↑⊤) G) (hGc : HasCompactSupport G) (i : Fin 3) : ∫ (x : Foundation.Parabolic.Vec3), spatialDeriv G i x = 0

The integral over all of Vec3 of a spatial partial derivative of a smooth compactly supported function vanishes. This is integration by parts against the constant test function 1, whose derivative is zero.

theorem CKN.lin34_integral_mixedSecond_eq_zero {G : Foundation.Parabolic.Vec3 → ℝ} (hG : ContDiff ℝ (↑⊤) G) (hGc : HasCompactSupport G) (i j : Fin 3) : ∫ (x : Foundation.Parabolic.Vec3), mixedSecond G i j x = 0

The integral over all of Vec3 of a mixed second derivative of a smooth compactly supported function vanishes: it is the spatial derivative of the smooth compactly supported function ∂_j G, so the previous integration-by-parts fact applies.

theorem CKN.lin34_constant_hessian_pairing_zero {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Ω : Set Foundation.Parabolic.Vec3} {s : ℝ} {b : Foundation.Parabolic.Vec3} {F : Foundation.Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hFc : HasCompactSupport F) (hFΩ : tsupport F ⊆ Ω) (hint : ∀ (j : Fin 3), MeasureTheory.IntegrableOn (fun (x : Foundation.Parabolic.Vec3) => u (x, s) j) (tsupport F) MeasureTheory.volume) (hdiv : ∀ (i : Fin 3), ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ j : Fin 3, u (x, s) j * mixedSecond F j i x = 0) : ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), b i * (u (x, s) j - b j) * mixedSecond F i j x = 0

The correction U_ij - Û_ij = -c_i (u_j - c_j) relating the singly and doubly centred nonlinearities of eq:Uhat of paper/ckn.tex pairs to zero against the Hessian of every smooth compactly supported test function F supported in Ω. Indeed the constant vector field b is divergence free, so the b_i b_j part of the pairing vanishes termwise, while the b_i u_j part is the divergence-free pairing ∫_Ω ∑_j u_j ∂_j ∂_i F supplied by hdiv; the two groups are related by the symmetry ∂_i ∂_j F = ∂_j ∂_i F of the Hessian.