Hessian L2

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

theorem CKN.pressure_neg_kernel_locallyIntegrable : MeasureTheory.LocallyIntegrable (fun (z : Foundation.Parabolic.Vec3) => -Foundation.Heat.newtonianKernel z) MeasureTheory.volume

theorem CKN.smooth_integration_by_parts {u φ : Foundation.Parabolic.Vec3 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (i : Fin 3) : ∫ (x : Foundation.Parabolic.Vec3), u x * spatialDeriv φ i x = -∫ (x : Foundation.Parabolic.Vec3), spatialDeriv u i x * φ x

theorem CKN.pressureNewtonianPotential_smooth {F : Foundation.Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hFc : HasCompactSupport F) : ContDiff ℝ (↑⊤) (pressureNewtonianPotential F)

theorem CKN.pressureNewtonianPotential_spatialDeriv_convolution {F : Foundation.Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hFc : HasCompactSupport F) (i : Fin 3) (x : Foundation.Parabolic.Vec3) : spatialDeriv (pressureNewtonianPotential F) i x = ∫ (y : Foundation.Parabolic.Vec3), spatialDeriv F i y * -Foundation.Heat.newtonianKernel (x - y)

theorem CKN.pressureNewtonianPotential_laplacian_eq {F : Foundation.Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hFc : HasCompactSupport F) (x : Foundation.Parabolic.Vec3) : spatialLaplacian (pressureNewtonianPotential F) x = F x

theorem CKN.hessian_l2_eq_laplacian_l2 {u : Foundation.Parabolic.Vec3 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (huc : HasCompactSupport u) : ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), mixedSecond u i j x ^ 2 = ∫ (x : Foundation.Parabolic.Vec3), spatialLaplacian u x ^ 2

The squared L² Hessian norm equals the squared L² Laplacian norm for a smooth compactly supported scalar function on Vec3.

theorem CKN.riesz_second_l2_bound {u : Foundation.Parabolic.Vec3 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (huc : HasCompactSupport u) (i j : Fin 3) : ∫ (x : Foundation.Parabolic.Vec3), mixedSecond u i j x ^ 2 ≤ ∫ (x : Foundation.Parabolic.Vec3), spatialLaplacian u x ^ 2