Integral Of A Trace Against A Mean Identity Matrix

This statement describes integration of a matrix trace against a matrix field whose entrywise mean is the identity.

Let Ω be a measurable space, ρ a measure on Ω, and ι a finite index type with decidable equality. Let H:Ω→Matrix(ι,ι,ℝ). Assume every entry $H_{ij}$ is integrable and has mean

Then for every real matrix B, the function $y\mapsto\operatorname{tr}(BH(y))$ is integrable and

This is a finite-coordinate linearity lemma for matrix-valued integration.

Formalization Note The hypothesis is entrywise and does not require H or B to be symmetric, positive, or measurable as a bundled matrix-valued function.

Original Lean declaration header

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

set_option maxHeartbeats 400000 in
theorem integral_trace_mul_of_mean_one {Ω ι : Type*} [MeasurableSpace Ω]
    [Fintype ι] [DecidableEq ι] (ρ : Measure Ω) (H : Ω → Matrix ι ι ℝ)
    (hInt : ∀ i j, Integrable (fun y => H y i j) ρ)
    (hmean : ∀ i j, (∫ y, H y i j ∂ρ) = (1 : Matrix ι ι ℝ) i j)
    (B : Matrix ι ι ℝ) :
    Integrable (fun y => Matrix.trace (B * H y)) ρ ∧
      (∫ y, Matrix.trace (B * H y) ∂ρ) = Matrix.trace B

Module navigation

Module: Analysis/Matrix/Integral.

Previous: symmetric_trace_integral_extension_mul_of_ae_posSemidef.

Source excerpt, lines 188–195 · Frozen source 408915f.