ProjectionStarter

Orthogonal projection and best approximation along a line

Open in Workbench View on GitHub

1-- Orthogonal projection and best approximation along a line2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module ProjectionStarter8import Grace.Cumulus.LinearAlgebra910theorem perpendicular_error (u v : RealSequence, n : Nat)11  requires nonzero : squaredNorm(v, n) ≠ 012  shows Orthogonal(subSequence(u, lineProjection(u, v, n)), v, n)13proof14  exact lineProjection.orthogonal at u, v, n with *1516theorem best_approximation (u v : RealSequence, C : Real, n : Nat)17  requires nonzero : squaredNorm(v, n) ≠ 018  shows lineDistanceSquared(u, v, projectionCoefficient(u, v, n), n) ≤19    lineDistanceSquared(u, v, C, n)20proof21  exact lineProjection.minimum at u, v, C, n with *2223theorem unique_best_coefficient (u v : RealSequence, C : Real, n : Nat)24  requires nonzero : squaredNorm(v, n) ≠ 025  requires minimizing : lineDistanceSquared(u, v, C, n) ≤26    lineDistanceSquared(u, v, projectionCoefficient(u, v, n), n)27  shows C = projectionCoefficient(u, v, n)28proof29  exact lineProjection.unique_minimizer at u, v, C, n with *3031-- This is one unnormalized Gram–Schmidt step in any finite dimension.32theorem orthogonal_decomposition (u v : RealSequence, n : Nat)33  requires nonzero : squaredNorm(v, n) ≠ 034  shows squaredNorm(u, n) = squaredNorm(lineProjection(u, v, n), n) +35    squaredNorm(orthogonalResidual(u, v, n), n)36proof37  exact orthogonalResidual.pythagorean at u, v, n with *3839theorem projecting_twice (u v : RealSequence, n : Nat)40  requires nonzero : squaredNorm(v, n) ≠ 041  shows lineProjection(lineProjection(u, v, n), v, n) = lineProjection(u, v, n)42proof43  exact lineProjection.idempotent at u, v, n with *44