Extension of Trace Integral Bounds to Symmetric Matrices

This is the almost-everywhere positive-semidefinite extension step associated with Theorem 2.5 of Letwin (arXiv:2607.24164v1).

Let $\iota$ be a finite index type with decidable equality, let $(\Omega,\nu)$ be an arbitrary measurable space with measure $\nu$, let $C\in\mathbb R$, and let $H:\Omega\to\operatorname{Matrix}(\iota,\iota,\mathbb R)$. Assume:

1. every entry of $H$ is measurable;
2. $H(x)$ is positive semidefinite for $\nu$-almost every $x$;
3. for every positive semidefinite matrix $A$, the function $x\mapsto\operatorname{tr}(AH(x)AH(x))$ is $\nu$-integrable and

Then every symmetric matrix $B$ has the same integrability and bound:

The theorem transfers a hypothesis stated only for positive semidefinite test matrices to all symmetric test matrices.

Formalization Note The coefficient $C$ has no sign assumption, $\nu$ need not be finite, and all positivity and almost-everywhere assertions use the stated matrix and measure-theoretic notions.

Original Lean declaration header

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

theorem symmetric_trace_integral_extension_mul_of_ae_posSemidef
    {Ω : Type*} [MeasurableSpace Ω] (ν : Measure Ω) {C : ℝ}
    (H : Ω → Matrix ι ι ℝ)
    (hH_meas : ∀ i j, Measurable (fun x => H x i j))
    (hH_psd : ∀ᵐ x ∂ν, (H x).PosSemidef)
    (hPSD : ∀ A : Matrix ι ι ℝ, A.PosSemidef →
      Integrable (fun x => (A * H x * A * H x).trace) ν ∧
        (∫ x, (A * H x * A * H x).trace ∂ν) ≤
          C * (A * A).trace)
    {B : Matrix ι ι ℝ} (hB : B.IsSymm) :
    Integrable (fun x => (B * H x * B * H x).trace) ν ∧
      (∫ x, (B * H x * B * H x).trace ∂ν) ≤
        C * (B * B).trace

Module navigation

Module: Analysis/Matrix/Integral.

Supporting theorems: jordan_trace_domination, symmetric_jordan_decomposition, trace_energy_nonneg.

Next: integral_trace_mul_of_mean_one.

Source excerpt, lines 32–44 · Frozen source 408915f.