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