norm_orthogonalProjection — Mathlib

English

If K is nontrivial, the operator norm of the orthogonal projection is exactly 1.

Русский

Если K непростое подпространство, операторная норма ортогональной проекции равна 1.

LaTeX

$$$ \|K.orthogonalProjection\| = 1 \quad\text{iff } K \neq \{0\}$$$

Lean4

/-- The operator norm of the orthogonal projection onto a nontrivial subspace is `1`. -/
theorem norm_orthogonalProjection (hK : K ≠ ⊥) : ‖K.orthogonalProjection‖ = 1 :=
  by
  refine le_antisymm K.orthogonalProjection_norm_le ?_
  obtain ⟨x, hxK, hx_ne_zero⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hK
  simpa [K.norm_orthogonalProjection_apply hxK, norm_eq_zero, hx_ne_zero] using K.orthogonalProjection.ratio_le_opNorm x

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