Integrability of a random symmetric matrix

A symmetric matrix is determined by its entries above the diagonal, and reading them off is a continuous linear equivalence with a finite product of copies of ℝ. A random symmetric matrix is therefore Bochner integrable exactly when each of its entries is, which is how the moments of a symmetric-matrix law are computed entry by entry.

theorem TauCeti.integrable_iff_integrable_coe_apply {p : ℕ} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} : MeasureTheory.Integrable f μ ↔ ∀ (i j : Fin p), MeasureTheory.Integrable (fun (ω : Ω) => ↑(f ω) i j) μ

A random symmetric matrix is integrable exactly when all of its entries are.