Integrals of positive-semidefinite matrices

An entrywise integral of an almost everywhere positive-semidefinite family of real matrices is positive semidefinite: its quadratic form is the integral of the pointwise quadratic forms. This is how positive semidefiniteness passes from a pointwise identity to a matrix of moments, such as the connection matrices of a homomorphism density.

Main results

• TauCeti.posSemidef_integral — the entrywise integral of an a.e. positive-semidefinite family of finite real matrices with integrable entries is positive semidefinite.

theorem TauCeti.posSemidef_integral {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Finite ι] {M : α → Matrix ι ι ℝ} (hM : ∀ᵐ (x : α) ∂μ, (M x).PosSemidef) (hint : ∀ (i j : ι), MeasureTheory.Integrable (fun (x : α) => M x i j) μ) : (Matrix.of fun (i j : ι) => ∫ (x : α), M x i j ∂μ).PosSemidef

The entrywise integral of positive-semidefinite matrices is positive semidefinite: if M x is positive semidefinite for almost every x and every entry of M is integrable, then the matrix of entrywise integrals is positive semidefinite.