Sum of Matrix Entry Variances as a Trace Difference

This is a finite-dimensional random-matrix variance identity.

Let $\mu$ be a probability measure on a measurable space $\alpha$. Let $H:\alpha\to\mathbb R^{n\times n}$ be almost-everywhere symmetric, with every entry in $L^2(\mu)$, and let $M\in\mathbb R^{n\times n}$ be symmetric. Assume that $M_{ij}=\int H_{ij}(x)\,d\mu(x)$ for every $i,j$. Then

This identity converts entrywise variance sums into trace expressions and is reusable in Hessian and matrix-energy estimates.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability. Shown in its original module context. Proof omitted.

theorem sum_variance_entries_eq_integral_trace_sub_trace_mean {alpha : Type*} [MeasurableSpace alpha]
    {n : ℕ} (mu : Measure alpha) [IsProbabilityMeasure mu]
    (H : alpha → Matrix (Fin n) (Fin n) ℝ) (M : Matrix (Fin n) (Fin n) ℝ)
    (hM : M.IsSymm) (hH : ∀ᵐ x ∂mu, (H x).IsSymm)
    (hH2 : ∀ i j, MemLp (fun x => H x i j) 2 mu)
    (hmean : ∀ i j, (∫ x, H x i j ∂mu) = M i j) :
    (∑ p : Fin n × Fin n, ProbabilityTheory.variance (fun x => H x p.1 p.2) mu) =
      (∫ x, (H x * H x).trace ∂mu) - (M * M).trace

Module navigation

Module: Probability/Moments.

Supporting theorems: sum_matrix_product_entry_mul_eq_trace.

Next: memLp_quadratic_of_memLp_four.

Source excerpt, lines 469–476 · Frozen source 408915f.