Symmetry of the completed second derivative

theorem CKN.Foundation.Euclidean.rieszSecondL2Extension_selfAdjoint {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (u v : ↥rieszSecondL2) : inner ℝ ((rieszSecondL2Extension hL2) u) v = inner ℝ u ((rieszSecondL2Extension hL2) v)

The completed L² second derivative is symmetric for the real inner product.

theorem CKN.Foundation.Euclidean.rieszSecondL2RawOperator_integral_mul_commute {i j : Fin 3} (hL2 : RieszSecondL2Input i j) {f g : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : ∫ (x : Parabolic.Vec3), rieszSecondL2RawOperator hL2 f x * g x = ∫ (x : Parabolic.Vec3), f x * rieszSecondL2RawOperator hL2 g x

The raw representative has the symmetric integral pairing on L² data.