Identification L2

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

theorem CKN.Foundation.Euclidean.rieszSecondL2_distributional_identity {i j : Fin 3} (hL2 : RieszSecondL2Input i j) {ψ : Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (g : ↥rieszSecondL2) : ∫ (x : Parabolic.Vec3), rieszSecondL2MeasurableOperator hL2 g x * spatialLaplacian ψ x = ∫ (x : Parabolic.Vec3), ↑↑g x * mixedSecond ψ i j x

The indexed L² second-order operator satisfies the test-function distributional identity on compactly supported smooth data and, by L² continuity, on every L² class.