starProjection_singleton — Mathlib

English

If ||v|| = 1, then projection onto span{v} is ⟨v,w⟩ v.

Русский

Если ||v|| = 1, то проекция на span{v} равна ⟨v,w⟩ v.

LaTeX

$$$ (\|v\| = 1) \Rightarrow (\mathrm{Proj}_{\mathbb{K}v}(w) = \langle v,w\rangle \; v) $$$

Lean4

/-- Formula for orthogonal projection onto a single vector. -/
theorem starProjection_singleton {v : E} (w : E) : (𝕜 ∙ v).starProjection w = (⟪v, w⟫ / ((‖v‖ ^ 2 : ℝ) : 𝕜)) • v :=
  by
  by_cases hv : v = 0
  · rw [hv]
    simp [Submodule.span_zero_singleton 𝕜]
  have hv' : ‖v‖ ≠ 0 := ne_of_gt (norm_pos_iff.mpr hv)
  have key :
    (((‖v‖ ^ 2 : ℝ) : 𝕜)⁻¹ * ((‖v‖ ^ 2 : ℝ) : 𝕜)) • ((𝕜 ∙ v).starProjection w) = (((‖v‖ ^ 2 : ℝ) : 𝕜)⁻¹ * ⟪v, w⟫) • v :=
    by simp [mul_smul, smul_starProjection_singleton 𝕜 w, -map_pow]
  convert key using 1 <;> match_scalars <;> field_simp [hv']

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