Spectral Noise Energy Bound

This is a finite-dimensional matrix-energy estimate with the trace bound supplied as a hypothesis.

Let $\rho$ and $\gamma$ be probability measures on measurable spaces $\Omega$ and $\Delta$. Let $H:\Omega\to\mathbb R^{n\times n}$ have measurable entries, be symmetric almost everywhere, have integrable entries, and have mean $I$. Assume that for every symmetric matrix $B$, $\operatorname{tr}(BH B H)$ is integrable and

Let $M$ be symmetric and invertible, and let $t\in\mathbb R$. Define $B=\sqrt{M^2}$, $S=\sqrt B$, and $Q=\operatorname{sign}(M)$. Then each coordinate energy is integrable and

No log-concavity or Stein-kernel conclusion is part of the statement; the trace estimate is an input.

Original Lean declaration header

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

set_option maxHeartbeats 1000000 in
theorem sum_integral_spectral_noise_energy_le {n : ℕ} {Ω Δ : Type*}
    [MeasurableSpace Ω] [MeasurableSpace Δ] (ρ : Measure Ω) [IsProbabilityMeasure ρ]
    (γ : Measure Δ) [IsProbabilityMeasure γ]
    (H : Ω → Matrix (Fin n) (Fin n) ℝ)
    (hHmeas : ∀ i j, Measurable (fun y => H y i j))
    (hHsym : ∀ᵐ y ∂ρ, (H y).IsSymm)
    (hHint : ∀ i j, Integrable (fun y => H y i j) ρ)
    (hmean : ∀ i j, (∫ y, H y i j ∂ρ) = (1 : Matrix (Fin n) (Fin n) ℝ) i j)
    (hT25 : ∀ B : Matrix (Fin n) (Fin n) ℝ, B.IsSymm →
      Integrable (fun y => Matrix.trace (B*H y*B*H y)) ρ ∧
        (∫ y, Matrix.trace (B*H y*B*H y) ∂ρ) ≤ 2*Matrix.trace (B*B))
    (M : Matrix (Fin n) (Fin n) ℝ) (hM : M.IsSymm) (hunit : IsUnit M) (t : ℝ) :
    let B : Matrix (Fin n) (Fin n) ℝ := CFC.sqrt (M*M)
    let S : Matrix (Fin n) (Fin n) ℝ := CFC.sqrt B
    let Q : Matrix (Fin n) (Fin n) ℝ := cfc (fun x : ℝ => (SignType.sign x : ℝ)) M
    (∀ i : Fin n, Integrable (fun y => ‖action (S*H y*S + t • 1)
      (action Q (EuclideanSpace.single i 1))‖^2) ρ) ∧
    (∑ i : Fin n, ∫ p : Ω × Δ, ‖action (S*H p.1*S + t • 1)
      (action Q (EuclideanSpace.single i 1))‖^2 ∂ρ.prod γ) ≤
      2*Matrix.trace (M*M) + 2*t*Matrix.trace B + (n : ℝ)*t^2

Module navigation

Module: Probability/Stein/QuadraticAction.

Definition modules: Analysis/Operator/Coordinates, Probability/Stein/Kernel.

Supporting theorems: integral_trace_mul_of_mean_one, symmetric_matrix_spectral_geometry.

Source excerpt, lines 66–86 · Frozen source 408915f.