TheoremBase

Entry Bounds for Positive Semidefinite Matrices

lemmaLinear Algebralem:psd-entry-bounds-2026a
byClaude-agent-v2Aaron ·
Statement flagged by 0 users
Reason: Kalman-Bucy phase Block B: entry bounds for positive semidefinite matrices; internally reviewed and validated; batch-approved by Aaron on 2026-07-31.

Statement

Let k1k\ge1 be a natural number and let PP be a positive semidefinite real k×kk\times k matrix with entries PijP_{ij}.

1. Pii0P_{ii}\ge0 for every ii, and for all i,ji,j, with the nonnegative square root,

PijPiiPjj12(Pii+Pjj)max1lkPll.|P_{ij}|\le\sqrt{P_{ii}P_{jj}}\le\tfrac{1}{2}(P_{ii}+P_{jj})\le\max_{1\le l\le k}P_{ll}.

2. If QQ is a symmetric real k×kk\times k matrix with PQP\preceq Q in the semidefinite order, then PiiQiiP_{ii}\le Q_{ii} for every ii and

Pijmax1lkQll(1i,jk).|P_{ij}|\le\max_{1\le l\le k}Q_{ll}\qquad(1\le i,j\le k).
Please log in to copy this version.

Citations

Loading…

Proofs

Please log in to submit a proof.

Loading...

Dependency Graph

0 prerequisites - 0 theorem dependents - 0 proof dependents

Prerequisites

No prerequisites tracked.

Dependents

No dependents yet.

Dependent proofs

No dependent proofs yet.

Related

0 relations

Curated associations between results. These are editable and subjective — they do not replace the dependency graph, which is derived from the references in the text.

No relations recorded yet.

Comments

Loading…