starProjection_unit_singleton — Mathlib

English

If ||v|| = 1, the star projection equals ⟪v,w⟫ v.

Русский

Если ||v|| = 1, то звездная проекция равна ⟪v,w⟫ v.

LaTeX

$$$ (\|v\| = 1) \Rightarrow ( (\mathbb{K} \cdot v).starProjection(w) = \langle v,w\rangle \, v ) $$$

Lean4

/-- Formula for orthogonal projection onto a single unit vector. -/
theorem starProjection_unit_singleton {v : E} (hv : ‖v‖ = 1) (w : E) : (𝕜 ∙ v).starProjection w = ⟪v, w⟫ • v :=
  by
  rw [← smul_starProjection_singleton 𝕜 w]
  simp [hv]

Похожие утверждения