re_inner_starProjection_eq_normSq

English

The starProjection onto K is a symmetric projection.

Русский

Звёздочная проекция на K является симметричной проекцией.

LaTeX

$$$ K.starProjection.IsSymmetricProjection. $$$

Lean4

theorem re_inner_starProjection_eq_normSq [K.HasOrthogonalProjection] (v : E) :
    re ⟪K.starProjection v, v⟫ = ‖K.orthogonalProjection v‖ ^ 2 :=
  by
  rw [starProjection_apply, re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two,
    div_eq_iff (NeZero.ne' 2).symm, pow_two, add_sub_assoc, ← eq_sub_iff_add_eq', coe_norm, ← mul_sub_one,
    show (2 : ℝ) - 1 = 1 by norm_num, mul_one, sub_eq_iff_eq_add', norm_sub_rev]
  exact orthogonalProjectionFn_norm_sq K v

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