smul_starProjection_singleton — Mathlib

English

Projection of w onto the line spanned by v is the scalar ⟨v,w⟩/⟨v,v⟩ times v.

Русский

Проекция w на прямую, порождаемую v, равна скаляру ⟨v,w⟩/⟨v,v⟩, умноженному на v (если v ≠ 0).

LaTeX

$$$ \mathrm{Proj}_{\mathbb{K}v}(w) = \dfrac{\langle v,w\rangle}{\langle v,v\rangle} \; v \quad (v \neq 0) $$$

Lean4

theorem smul_starProjection_singleton {v : E} (w : E) : ((‖v‖ ^ 2 : ℝ) : 𝕜) • (𝕜 ∙ v).starProjection w = ⟪v, w⟫ • v :=
  by
  suffices ((𝕜 ∙ v).starProjection (((‖v‖ : 𝕜) ^ 2) • w)) = ⟪v, w⟫ • v by simpa using this
  apply eq_starProjection_of_mem_of_inner_eq_zero
  · rw [Submodule.mem_span_singleton]
    use ⟪v, w⟫
  · rw [← Submodule.mem_orthogonal', Submodule.mem_orthogonal_singleton_iff_inner_left]
    simp [inner_sub_left, inner_smul_left, inner_self_eq_norm_sq_to_K, mul_comm]

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