norm_orthogonalProjection_apply_le

English

The norm of the orthogonal projection is bounded by the norm of the original vector.

Русский

Норма ортогональной проекции не превосходит норму исходного вектора.

LaTeX

$$$ \|\mathrm{orthogonalProjection}_K(v)\| \leq \|v\| \quad \text{for all } v \in E $$$

Lean4

/-- The orthogonal projection onto a closed subspace is norm non-increasing. -/
theorem norm_orthogonalProjection_apply_le (v : E) : ‖orthogonalProjection K v‖ ≤ ‖v‖ := by
  calc
    ‖orthogonalProjection K v‖ ≤ ‖orthogonalProjection K‖ * ‖v‖ := K.orthogonalProjection.le_opNorm _
    _ ≤ 1 * ‖v‖ := by gcongr; exact orthogonalProjection_norm_le K
    _ = _ := by simp

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