Inner products and the spectral theorem

The scalar product (u, v) = u₁v₁ + … + u_nv_n measures how much two vectors point the same way. Its square root of (u, u) is the length. Two facts make the geometry work: the product of lengths is never smaller than the size of the scalar product (Schwarz), so an angle can be defined, and the length of a sum is never more than the sum of lengths (triangle). When the scalar product is zero the vectors are perpendicular, and then the lengths obey Pythagoras.

Schwarz. If y = 0 both sides are 0. Otherwise, for every real t, 0 ≤ (x − ty, x − ty) = |x|² − 2t(x, y) + t²|y|². Take t = (x, y)/|y|²: this gives 0 ≤ |x|² − (x, y)²/|y|², which is the inequality squared. Equality means (x − ty, x − ty) = 0, so x = ty by positivity. □

Triangle. |x + y|² = |x|² + 2(x, y) + |y|² ≤ |x|² + 2|x||y| + |y|² = (|x| + |y|)² by Schwarz. Pythagoras is the same expansion with the middle term 0. □

Lax pp.77–80. Lean: schwarz, triangle and pythagoras are calls to Mathlib’s abs_real_inner_le_norm, norm_add_le and norm_add_sq_eq_norm_sq_add_norm_sq_real, stated for any real inner product space; compiled. For pythagoras the Mathlib lemma gives the squares as products, and one nlinarith step turns them into powers. The script checks Schwarz for all 15,625 ordered pairs of integer vectors in {−2,…,2}³; that equality holds exactly for proportional pairs; the triangle inequality exactly, through squares; and Pythagoras for every orthogonal pair. Controls: the form x₁y₁ − x₂y₂ is not positive, since (1,1) is not zero but has “length squared” 0, and Schwarz fails for it: u = (1,0), v = (2,1) give (u, v)² = 4 but (u, u)(v, v) = 1 × 3 = 3. Positivity is doing real work.

Given any basis, you can straighten it. Keep the first vector. From the second, subtract its shadow along the first. From the third, subtract its shadows along the first two. What is left of each is perpendicular to all earlier ones, and nothing is lost because each step only subtracts combinations of earlier vectors.

The step. Set x_k = y_k − ∑_j<k [(y_k, x_j)/(x_j, x_j)] x_j. For i < k, (x_k, x_i) = (y_k, x_i) − (y_k, x_i) = 0, because the earlier x_j are orthogonal to one another. And x_k is not zero, since otherwise y_k would be a combination of y₁, …, y_k−1. □

Example. y₁ = (1,1,0), y₂ = (1,0,1), y₃ = (0,1,1). Then x₁ = (1,1,0). For x₂: (y₂, x₁) = 1 and (x₁, x₁) = 2, so x₂ = (1,0,1) − ½(1,1,0) = (½, −½, 1). For x₃: the shadow on x₁ has coefficient 1/2 and on x₂ has coefficient (1/2)/(3/2) = 1/3, so x₃ = (0,1,1) − ½(1,1,0) − ⅓(½, −½, 1) = (−⅔, ⅔, ⅔). Check: (x₁, x₂) = ½ − ½ = 0, (x₁, x₃) = 0, (x₂, x₃) = −⅓ − ⅓ + ⅔ = 0.

Lean: not stated; Mathlib has Gram–Schmidt, and the file does not use it. The script runs the worked example in exact fractions, and 200 random integer bases of Q³ (fixed seed): in every case the output is mutually orthogonal and nonzero, and x₃ − y₃ lies in the span of y₁ and y₂, which is the triangular property. The output vectors are left unnormalised so everything stays rational.

Pick a subspace Y, say a line or a plane through the origin. Every vector splits uniquely into a part inside Y and a part perpendicular to Y. The inside part is the orthogonal projection: it is the point of Y nearest to the vector, because any other point of Y adds a sideways step at a right angle to the perpendicular, and by Pythagoras that only lengthens the trip.

The closest point. For z in Y, x − z = (x − Px) + (Px − z), where the first is in Y^⊥ and the second is in Y, so by Pythagoras |x − z|² = |x − Px|² + |Px − z|², which is larger unless z = Px. □

The formula. Write Px = Ac. The condition x − Ac ⊥ every column of A is A^T(x − Ac) = 0, that is A^TA c = A^Tx. A^TA is invertible when the columns are independent, because A^TAc = 0 gives |Ac|² = c^TA^TAc = 0, so Ac = 0 and c = 0. Then c = (A^TA)⁻¹A^Tx. □

Example. Project x = (3,1) onto the line through (1,1). The coefficient is (x, (1,1))/((1,1),(1,1)) = 4/2 = 2, so Px = (2,2) and the remainder is (1,−1), perpendicular to (1,1) because 1 − 1 = 0. Check by Pythagoras: |x|² = 10 = |Px|² + |x − Px|² = 8 + 2.

Lean: complement states that Y and Y^⊥ are complementary (IsCompl) in a finite-dimensional real inner product space, from Mathlib’s orthogonal-complement lemma; compiled, with a warning that the lemma used is deprecated in favour of Submodule.isCompl_orthogonal (left unchanged, it still works). The script checks, for 200 random integer 4×2 matrices with independent columns (fixed seed): P = A(A^TA)⁻¹A^T satisfies P² = P exactly, P is symmetric, x − Px is orthogonal to both columns, and no competitor Ac with c on a 17×17 grid of half-integers is closer to x than Px. That last check is an illustration of Theorem 8, not a proof.

Fitting a line to points that do not lie on one line is the same problem as finding the closest point. The data vector b is not in the range of the matrix A, so ask for the point of the range nearest to b. The answer is its projection, and the equations that say “the leftover is perpendicular to every column of A” are the normal equations A^TA c = A^Tb. This is the arithmetic behind linear regression in statistics.

Adjoint. (Ax, y) = ∑_i (∑_j a_ijx_j) y_i = ∑_j x_j (∑_i a_ijy_i) = (x, A^Ty). Least squares is Theorem 8 for the range of A, as in section 3. □

Example, four points. Fit y = c₀ + c₁t to (0,1), (1,2), (2,2), (3,4). The matrix A has rows (1,0), (1,1), (1,2), (1,3) and b = (1,2,2,4). Then A^TA = [[4,6],[6,14]] and A^Tb = (9,18). Since det A^TA = 56 − 36 = 20, the inverse is (1/20)[[14,−6],[−6,4]], and c = (1/20)(126 − 108, −54 + 72) = (9/10, 9/10). The line is y = 0.9 + 0.9 t, the fitted values are 0.9, 1.8, 2.7, 3.6, and the residuals are 0.1, 0.2, −0.7, 0.4. They add to 0 and are orthogonal to the t column (0.2 − 1.4 + 1.2 = 0). The sum of squared residuals is 0.01 + 0.04 + 0.49 + 0.16 = 7/10.

Lean: not stated. The script checks every number in the example in exact fractions: the normal equations [[4,6],[6,14]] and (9,18), the solution, the residuals, the sum 7/10, that no line with intercept and slope within 1/2 of the fit (441 lines, steps of 1/20) has a smaller sum of squares, and that moving the intercept by 1/10 adds exactly 4 × (1/10)² = 1/25, as Pythagoras predicts. Link to statistics. This is the computation behind the least-squares line of OpenIntro Statistics, chapter 8 (linear regression with a single predictor; about page 303 of the held copy, a reference the script does not check). What this chapter does not do is any of the statistics: no standard errors, no model assumptions.

A symmetric matrix A defines a quadratic form q(y) = (Ay, y), a bowl-shaped, saddle-shaped or trough-shaped function on the plane. Near a critical point, any smooth function of several variables looks like such a form built from its second derivatives, the Hessian, which is symmetric because mixed partial derivatives agree. So whether a critical point is a minimum, a maximum or a saddle is a question about the signs of a symmetric matrix.

Complete the square: if a ≠ 0, a y₁² + 2b y₁y₂ + d y₂² = a(y₁ + (b/a)y₂)² + (D/a) y₂². If a > 0 and D > 0 both terms are non-negative and they vanish together only at y = 0: positive definite. If D < 0 the two terms have opposite signs, so the form takes both signs. If D > 0 then a and d have the same sign (ad > b² ≥ 0), so a > 0 exactly when T > 0. The cases a = 0 are handled by d, or by D = −b² ≤ 0. □

Lean: not stated; the sign test is checked by the script, not by Lean. The script runs over all 343 symmetric integer matrices with entries from −3 to 3: 31 positive definite, 31 negative definite, 256 indefinite, 25 singular; for all 343 the two forms of the positive-definite test agree; and each positive-definite matrix has q(y) > 0 at all 48 nonzero y with entries in −3..3 (an illustration). The Hessian test for critical points (positive definite means local minimum) is Lax’s statement of a result from calculus; it is referenced here, not proved, and the script does not check it.

In chapter 7 a real matrix could have no real eigenvalue (a rotation), or too few eigenvectors (a shear). Symmetry rules out both. The reason in two dimensions is a one-line computation: the two eigenvectors, built from the entries, are automatically perpendicular. In every dimension the same thing holds, so a symmetric matrix is a stretching along a set of perpendicular axes, and those axes are the natural coordinates for the quadratic form.

Real roots. T² − 4D = (a + d)² − 4(ad − b²) = (a − d)² + 4b² ≥ 0. Eigenvector. Row one of (A − λI)(b, λ − a)^T is (a − λ)b + b(λ − a) = 0, and row two is b² + (d − λ)(λ − a) = b² − (λ² − Tλ + ad) = −(λ² − Tλ + D) = 0 when λ is a root. Orthogonal. The dot product is b² + (λ₁ − a)(λ₂ − a) = b² + λ₁λ₂ − a(λ₁ + λ₂) + a² = b² + D − aT + a² = b² + (ad − b²) − a(a + d) + a² = 0, using λ₁ + λ₂ = T and λ₁λ₂ = D. □

General case, in outline (the standard maximisation argument). Maximise the quadratic form (Ax, x) over unit vectors; the maximum is attained (the sphere is compact) at a vector h, and the Lagrange condition gives Ah = λh with λ real. The perpendicular complement of h is carried into itself by A (because (Ax, h) = (x, Ah) = λ(x, h) = 0 for x ⊥ h), so the argument repeats in one dimension fewer. This outline is not machine-checked here.

Example. A = [[2,1,1],[1,2,1],[1,1,2]]. A(1,1,1) = (4,4,4), and A(1,−1,0) = (1,−1,0), A(0,1,−1) = (0,1,−1), so the eigenvalues are 4, 1, 1, and (1,1,1) is perpendicular to the plane spanned by the other two. Then A = 4P₁ + 1P₂ with P₁ = (1/3)J (J all ones) the projection onto (1,1,1) and P₂ = I − P₁. For the 2×2 case A = [[2,1],[1,2]]: eigenvalues 3 and 1, eigenvectors (1,1) and (1,−1), dot product 0.

Lean: eigen_equation is the algebraic heart of the 2×2 orthogonality, proved by linear_combination from the two root equations; eigenbasis_orthonormal is Mathlib’s spectral theorem for symmetric linear maps, stated with an orthonormal basis and real eigenvalues; both compiled. The script checks, for all 343 matrices: the discriminant is non-negative; the 336 with distinct eigenvalues have orthogonal eigenvectors (b, λ − a) by the exact identity b² + D − aT + a² = 0; the other 7 are the scalar matrices. And the 3×3 decomposition above: P₁² = P₁, P₂² = P₂, P₁P₂ = 0, P₁ + P₂ = I, and 4P₁ + P₂ = A, all symmetric.

Controls: what symmetry and the reals each contribute. The symmetric matrix [[0,1],[1,1]] has no eigenvalue over F₃, because t² − t − 1 has no root there, so the theorem needs the real numbers. The complex symmetric matrix [[1,i],[i,−1]] is not zero but squares to zero, so its only eigenvalue is 0 and it is not diagonalisable: symmetry alone, without realness (it is symmetric but not Hermitian), is not enough. And the non-symmetric [[1,1],[0,1]] has one eigenvalue and one eigenvector line, so no orthogonal pair of eigenvectors. Each control breaks one hypothesis and the conclusion fails.

Four things are left out on purpose. Complex inner products, Hermitian and normal matrices, which are Lax’s setting for the full spectral theory, are not here. The singular value decomposition, which extends these ideas to non-square matrices, is not here. The existence of the maximum used in the outline of the general proof rests on compactness of the unit sphere, which is not proved in this chapter. And the second-derivative test for critical points of a function of several variables, which uses the Hessian, is stated as a reference to calculus, not proved. The step from this chapter to principal components in statistics (the eigenvectors of a covariance matrix) is an application of the spectral theorem and of a definition of covariance that this book does not yet give.