English
The orthogonal projection lies in the direction subspace, and the remainder lies in the orthogonal complement.
Русский
Ортогональная проекция лежит в направлении подплощадного пространства, а остаток лежит в его ортогональном дополнении.
LaTeX
$$$ \operatorname{orthogonalProjection}(s)p \in s.direction \quad \text{and} \quad p -\!\!>\!\! \operatorname{orthogonalProjection} s p \in s.direction^\perp $$$
Lean4
/-- Subtracting the `orthogonalProjection` from `p` produces a result in the kernel of the linear
part of the orthogonal projection. -/
theorem orthogonalProjection_vsub_orthogonalProjection (s : AffineSubspace ℝ P) [Nonempty s]
[s.direction.HasOrthogonalProjection] (p : P) :
s.direction.orthogonalProjection (p -ᵥ orthogonalProjection s p) = 0 :=
by
apply Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
intro c hc
rw [← neg_vsub_eq_vsub_rev, inner_neg_right, orthogonalProjection_vsub_mem_direction_orthogonal s p c hc, neg_zero]
