positive semidefinite concept
| Definition | Of a symmetric matrix, having every quadratic form nonnegative, as the read operator and the covariance are. Chapter 0 section 0.3. Also semidefinite. |
|---|---|
| Example | The matrix with rows (1, 2) and (2, 4) is positive semidefinite, and the one with rows (1, 3) and (3, 1) is not, since (1, −1) gives −4. |
| Book | Data Mining as Observation, draft 0.2, commit f3914f0; entry id positive-semidefinite, kind concept. |
| Status | no ledger row names this entry. Corrections: none recorded. |
| Defining equation | Book equation 0.9. |
| Assumptions and scope |
|
| Prior art | none recorded |
| Evidence | lean/DataMiningAsObservation/PositiveSemidefinite.lean |
| Reviewed | not yet reviewed; generated 2026-09-10 from records at the commits on the provenance page. |
Equation
Book equation 0.9.
\[P_C=\mathbb E\!\left[g\,g^{\top}\right],\qquad g=\nabla C(x).\]
Book equation 0.11.
\[P_C(x)=J(x)^{\top}G\big(C(x)\big)\,J(x),\qquad J(x)=\frac{\partial C}{\partial x}(x),\qquad \bar P_{C,\mu}=\mathbb E_{\mu}\!\left[P_C(x)\right].\]
Conditions
- Of a symmetric matrix, having every quadratic form nonnegative. A sum of such matrices is one, a nonnegative multiple is one, an outer product of a vector with itself is one, the read operator is one whenever the weights are nonnegative, and the diagonal entries are nonnegative.
- The local metric on a consumer’s output is positive semidefinite and exists only where the output metric has a local quadratic representation, and every eigenvalue of a positive semidefinite matrix is nonnegative.
Conditions are curated in entries.toml rather than read
from a record.
Ledger
none
First stated
Chapter 0 section 0.3 and section 0.5 of Data Mining as Observation.
Measurements
none
Failures and corrections
none
Invariance envelope
none declared
Machine checked
lean/DataMiningAsObservation/PositiveSemidefinite.lean,
theorems psd_add, psd_smul,
psd_outer, psd_readOp,
psd_diag_nonneg, at observation-data-mining f3914f0; what
the check covers is stated in the book’s appendix
C.
Used in
Data Mining as Observation primer L, chapters 0, 2.
Related
read operator; covariance matrix; outer product; eigenvalue, eigenvector; metric.
See also
Book equations stated beside the entry’s terms, not defining it: 0.3.
Ledger rows that cite the entry’s records without naming it: OT-7.
Sources-table rows that share a record with the entry without naming it: chapter 2 section 2.2.
Status
Generated 2026-09-10 by encyclopedia/generate.py; book
at observation-data-mining f3914f0; the commit of every record is listed
in the encyclopedia’s provenance.