re_inner_starProjection_nonneg — Mathlib

English

The real part of the inner product of P_K v and v equals the square of the norm of the projection onto K, i.e., re ⟪P_K v, v⟫ = ||P_K v||^2.

Русский

Действительная часть скалярного произведения ⟪P_K v, v⟫ равна квадрату нормы проекции на K.

LaTeX

$$$ \operatorname{Re}\langle K.\!starProjection(v), v \rangle = \|K.\!orthogonalProjection(v)\|^2. $$$

Lean4

theorem re_inner_starProjection_nonneg [K.HasOrthogonalProjection] (v : E) : 0 ≤ re ⟪K.starProjection v, v⟫ :=
  by
  rw [re_inner_starProjection_eq_normSq K v]
  exact sq_nonneg ‖K.orthogonalProjection v‖

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