orthogonalProjectionFn_norm_sq — Mathlib

English

The norm decomposition identity holds: ||v||^2 = ||v−p||^2 + ||p||^2 where p = K.orthogonalProjectionFn(v).

Русский

Существуют формула разложения нормы: ||v||^2 = ||v−p||^2 + ||p||^2, где p = K.orthogonalProjectionFn(v).

LaTeX

$$‖v‖^2 = ‖v−K.orthogonalProjectionFn(v)‖^2 + ‖K.orthogonalProjectionFn(v)‖^2$$

Lean4

theorem orthogonalProjectionFn_norm_sq (v : E) :
    ‖v‖ * ‖v‖ =
      ‖v - K.orthogonalProjectionFn v‖ * ‖v - K.orthogonalProjectionFn v‖ +
        ‖K.orthogonalProjectionFn v‖ * ‖K.orthogonalProjectionFn v‖ :=
  by
  set p := K.orthogonalProjectionFn v
  have h' : ⟪v - p, p⟫ = 0 := orthogonalProjectionFn_inner_eq_zero _ _ (orthogonalProjectionFn_mem v)
  convert norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (v - p) p h' using 2 <;> simp

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