Shared skew-field identities

Smooth-test density and finite-dimensional antisymmetry identities extracted from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46.

theorem Algsuperdiff.StochasticProcess.Common.DivergenceForm.integral_vecDot_congr_of_forall_smooth {d : ℕ} {U : Set (HCPolySupport.Vec d)} {P Q : HCPolySupport.Vec d → HCPolySupport.Vec d} (hP : ∀ (i : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => P x i) (hQ : ∀ (i : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => Q x i) (hsmooth : ∀ (psi : HCPolySupport.Vec d → ℝ), ContDiff ℝ (↑⊤) psi → HasCompactSupport psi → tsupport psi ⊆ U → ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (P x) (HCPolySupport.euclideanGradient psi x) = ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (Q x) (HCPolySupport.euclideanGradient psi x)) (phi : HCPolySupport.H10Function U) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (P x) (phi.grad x) = ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (Q x) (phi.grad x)

Smooth compact tests determine the zero-trace gradient pairing.

theorem Algsuperdiff.StochasticProcess.Common.DivergenceForm.sum_sum_mul_eq_zero_of_skew_of_symm {d : ℕ} {K : HCPolySupport.Mat d} (hK : ∀ (i j : Fin d), K j i = -K i j) {T : Fin d → Fin d → ℝ} (hT : ∀ (i j : Fin d), T i j = T j i) : ∑ i : Fin d, ∑ j : Fin d, K i j * T i j = 0

Contracting an antisymmetric matrix with a symmetric matrix gives zero.