Grace/Cumulus/LinearAlgebra/Orthogonalization.g17

Open in Workbench Download source

Imports

Projection

Declarations

Source

1-- Orthogonality invariants for successive projection removal2-- 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 Grace.Cumulus.LinearAlgebra.Orthogonalization8import Projection910-- Removing a component along v leaves every inner product with a direction11-- perpendicular to v unchanged. No nonzero-norm premise is needed here.12theorem dotProduct.after_orthogonal_removal (u v w : Set, n : Nat)13  requires sequenceU : RealSequence(u)14  requires sequenceV : RealSequence(v)15  requires sequenceW : RealSequence(w)16  requires perpendicular : Orthogonal(v, w, n)17  shows dotProduct(orthogonalResidual(u, v, n), w, n) = dotProduct(u, w, n)18proof19  unfold Orthogonal at perpendicular20  unfold orthogonalResidual21  rw dotProduct.sub_left22  unfold lineProjection23  rw [dotProduct.scale_left, perpendicular]24  ring2526theorem orthogonalResidual.preserve_orthogonal (u v w : Set, n : Nat)27  requires sequenceU : RealSequence(u)28  requires sequenceV : RealSequence(v)29  requires sequenceW : RealSequence(w)30  requires old : Orthogonal(u, w, n)31  requires directions : Orthogonal(v, w, n)32  shows Orthogonal(orthogonalResidual(u, v, n), w, n)33proof34  unfold Orthogonal at old35  unfold Orthogonal36  rwa dotProduct.after_orthogonal_removal3738theorem projectionCoefficient.after_orthogonal_removal (u v w : Set, n : Nat)39  requires sequenceU : RealSequence(u)40  requires sequenceV : RealSequence(v)41  requires sequenceW : RealSequence(w)42  requires perpendicular : Orthogonal(v, w, n)43  shows projectionCoefficient(orthogonalResidual(u, v, n), w, n) = projectionCoefficient(u, w, n)44proof45  have unchanged := dotProduct.after_orthogonal_removal at u, v, w, n with *46  simp [projectionCoefficient]4748theorem lineProjection.after_orthogonal_removal (u v w : Set, n : Nat)49  requires sequenceU : RealSequence(u)50  requires sequenceV : RealSequence(v)51  requires sequenceW : RealSequence(w)52  requires perpendicular : Orthogonal(v, w, n)53  shows lineProjection(orthogonalResidual(u, v, n), w, n) = lineProjection(u, w, n)54proof55  have unchanged := projectionCoefficient.after_orthogonal_removal at u, v, w, n with *56  simp [lineProjection]5758theorem orthogonalResidual.orthogonal_pair (u v w : Set, n : Nat)59  requires sequenceU : RealSequence(u)60  requires sequenceV : RealSequence(v)61  requires sequenceW : RealSequence(w)62  requires nonzeroV : squaredNorm(v, n) ≠ (0:R)63  requires nonzeroW : squaredNorm(w, n) ≠ (0:R)64  requires perpendicular : Orthogonal(v, w, n)65  shows Orthogonal(orthogonalResidual(orthogonalResidual(u, v, n), w, n), v, n) ∧66    Orthogonal(orthogonalResidual(orthogonalResidual(u, v, n), w, n), w, n)67proof68  have firstOrthogonal := orthogonalResidual.orthogonal at u, v, n with *69  have symmetric := Orthogonal.symmetric at v, w, n with *70  constructor71  . exact orthogonalResidual.preserve_orthogonal with *72  . exact orthogonalResidual.orthogonal with *7374theorem orthogonalResidual.two_step_reconstruction (u v w : Set, n i : Nat)75  requires sequenceU : RealSequence(u)76  requires sequenceV : RealSequence(v)77  requires sequenceW : RealSequence(w)78  requires perpendicular : Orthogonal(v, w, n)79  shows u[i] = (lineProjection(u, v, n)[i]:R) + (lineProjection(u, w, n)[i]:R) +80    (orthogonalResidual(orthogonalResidual(u, v, n), w, n)[i]:R)81proof82  have firstReconstruction := orthogonalResidual.reconstruction at u, v, n, i with *83  have secondReconstruction := orthogonalResidual.reconstruction at orthogonalResidual(u, v, n), w, n, i with *84  have unchanged := lineProjection.after_orthogonal_removal at u, v, w, n with *85  rw unchanged at secondReconstruction86  linear_combination firstReconstruction + secondReconstruction8788theorem orthogonalResidual.two_step_pythagorean (u v w : Set, n : Nat)89  requires sequenceU : RealSequence(u)90  requires sequenceV : RealSequence(v)91  requires sequenceW : RealSequence(w)92  requires nonzeroV : squaredNorm(v, n) ≠ (0:R)93  requires nonzeroW : squaredNorm(w, n) ≠ (0:R)94  requires perpendicular : Orthogonal(v, w, n)95  shows squaredNorm(u, n) = squaredNorm(lineProjection(u, v, n), n) +96    squaredNorm(lineProjection(u, w, n), n) +97    squaredNorm(orthogonalResidual(orthogonalResidual(u, v, n), w, n), n)98proof99  have firstPythagorean := orthogonalResidual.pythagorean at u, v, n with *100  have secondPythagorean := orthogonalResidual.pythagorean at orthogonalResidual(u, v, n), w, n with *101  have unchanged := lineProjection.after_orthogonal_removal at u, v, w, n with *102  rw unchanged at secondPythagorean103  linear_combination firstPythagorean + secondPythagorean104105theorem orthogonalResidual.commute (u v w : Set, n i : Nat)106  requires sequenceU : RealSequence(u)107  requires sequenceV : RealSequence(v)108  requires sequenceW : RealSequence(w)109  requires perpendicular : Orthogonal(v, w, n)110  shows orthogonalResidual(orthogonalResidual(u, v, n), w, n)[i] =111    orthogonalResidual(orthogonalResidual(u, w, n), v, n)[i]112proof113  have symmetric := Orthogonal.symmetric with *114  have forward := orthogonalResidual.two_step_reconstruction at u, v, w, n, i with *115  have backward := orthogonalResidual.two_step_reconstruction at u, w, v, n, i with *116  linear_combination backward - forward117118-- Bessel's inequality for two perpendicular, not necessarily unit, directions.119-- The captured squared lengths cannot exceed the original squared length.120theorem lineProjection.bessel_pair (u v w : RealSequence, n : Nat)121  requires nonzeroV : squaredNorm(v, n) ≠ (0:R)122  requires nonzeroW : squaredNorm(w, n) ≠ (0:R)123  requires perpendicular : Orthogonal(v, w, n)124  shows squaredNorm(lineProjection(u, v, n), n) +125    squaredNorm(lineProjection(u, w, n), n) ≤ squaredNorm(u, n)126proof127  have decomposition := orthogonalResidual.two_step_pythagorean at u, v, w, n with *128  have remainderNonnegative := squaredNorm.nonnegative at orthogonalResidual(orthogonalResidual(u, v, n), w, n), n with *129  rw decomposition130  linarith131