Orthogonal decomposition in the planar quarter-turn basis

Proved

PlanarRot90Decomposition

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

crossing-consequencesgeometrypolygonal

Every vector in the Euclidean plane decomposes, relative to a nonzero direction $d$ , into its component along $d$ and its component along $\operatorname{PlanarRot90}(d)$ , with coefficients given by normalized inner products.

Preamble

import Definitions.Def_PlanarRot90

open Classical
noncomputable section

Formal statement

lemma PlanarRot90Decomposition (d v : EuclideanSpace ℝ (Fin 2)) (hd : d ≠ 0) :
    v =
      (inner ℝ v d / (‖d‖ ^ 2)) • d +
        (inner ℝ v (PlanarRot90 d) / (‖d‖ ^ 2)) • PlanarRot90 d := by sorry

Source

https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/PlanarRot90Decomposition.lean#L1-L69

View graph