orthogonal concept
| Definition | Of two vectors, having dot product zero. The squared length of a sum of orthogonal vectors is the sum of the squared lengths. Chapter 0 section 0.1. Also orthonormal. |
|---|---|
| Example | (1, 0) and (0, 1) are orthogonal, and the squared length of their sum is 1 + 1 = 2. |
| Book | Data Mining as Observation, draft 0.2, commit f3914f0; entry id orthogonal, kind concept. |
| Status | no ledger row names this entry. Corrections: none recorded. |
| Defining equation | Book equation 0.1. |
| Assumptions and scope |
|
| Prior art | none recorded |
| Evidence | lean/DataMiningAsObservation/Orthogonal.lean |
| Reviewed | not yet reviewed; generated 2026-09-10 from records at the commits on the provenance page. |
Equation
Book equation 0.1.
\[x\cdot y=\sum_{i=1}^{d}x_i y_i,\qquad \|x\|=\sqrt{x\cdot x},\qquad \cos\theta=\frac{x\cdot y}{\|x\|\,\|y\|}.\]
Conditions
- Of two vectors, having dot product zero. The relation is symmetric, survives rescaling, holds between any vector and zero, the squared length of a sum of orthogonal vectors is the sum of the squared lengths, and the residual of a projection is orthogonal to the direction projected on.
- A linear classifier’s nuisance is everything orthogonal to its weight vector, and the eigenvectors of a symmetric matrix with distinct eigenvalues are orthogonal, so the read subspace and the nuisance split every row.
Conditions are curated in entries.toml rather than read
from a record.
Ledger
none
First stated
Chapter 0 section 0.1 and section 0.2 of Data Mining as Observation.
Measurements
none
Failures and corrections
none
Invariance envelope
none declared
Machine checked
lean/DataMiningAsObservation/Orthogonal.lean,
theorems orth_symm, pythagoras,
orth_smul, orth_zero,
residual_orth, 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, 3, 4, 6, 9, 11, 12.
Related
dot product; projection; eigenvalue, eigenvector; nuisance; read subspace.
See also
Book equations stated beside the entry’s terms, not defining it: 0.3, 0.9.
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.