OrthogonalizationStarter

Successive removal of perpendicular components

Open in Workbench View on GitHub

1-- Successive removal of perpendicular components2-- 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 OrthogonalizationStarter8import Grace.Cumulus.LinearAlgebra910theorem preserve_previous_direction (u v w : RealSequence, n : Nat)11  requires old : Orthogonal(u, w, n)12  requires directions : Orthogonal(v, w, n)13  shows Orthogonal(orthogonalResidual(u, v, n), w, n)14proof15  exact orthogonalResidual.preserve_orthogonal at u, v, w, n with *1617theorem perpendicular_to_both (u v w : RealSequence, n : Nat)18  requires nonzeroV : squaredNorm(v, n) ≠ 019  requires nonzeroW : squaredNorm(w, n) ≠ 020  requires perpendicular : Orthogonal(v, w, n)21  shows Orthogonal(orthogonalResidual(orthogonalResidual(u, v, n), w, n), v, n) ∧22    Orthogonal(orthogonalResidual(orthogonalResidual(u, v, n), w, n), w, n)23proof24  exact orthogonalResidual.orthogonal_pair at u, v, w, n with *2526theorem order_independent (u v w : RealSequence, n i : Nat)27  requires perpendicular : Orthogonal(v, w, n)28  shows orthogonalResidual(orthogonalResidual(u, v, n), w, n)[i] =29    orthogonalResidual(orthogonalResidual(u, w, n), v, n)[i]30proof31  exact orthogonalResidual.commute at u, v, w, n, i with *3233theorem three_part_energy (u v w : RealSequence, n : Nat)34  requires nonzeroV : squaredNorm(v, n) ≠ 035  requires nonzeroW : squaredNorm(w, n) ≠ 036  requires perpendicular : Orthogonal(v, w, n)37  shows squaredNorm(u, n) = squaredNorm(lineProjection(u, v, n), n) +38    squaredNorm(lineProjection(u, w, n), n) +39    squaredNorm(orthogonalResidual(orthogonalResidual(u, v, n), w, n), n)40proof41  exact orthogonalResidual.two_step_pythagorean at u, v, w, n with *4243-- The two orthogonal components capture at most the original squared length.44theorem captured_energy (u v w : RealSequence, n : Nat)45  requires nonzeroV : squaredNorm(v, n) ≠ 046  requires nonzeroW : squaredNorm(w, n) ≠ 047  requires perpendicular : Orthogonal(v, w, n)48  shows squaredNorm(lineProjection(u, v, n), n) +49    squaredNorm(lineProjection(u, w, n), n) ≤ squaredNorm(u, n)50proof51  exact lineProjection.bessel_pair at u, v, w, n with *52