entrywise_sup_norm_bound_of_unitary

English

The operator norm of a unitary matrix U is at most 1: ||U|| ≤ 1.

Русский

Пусть U — унитарная матрица; нормa оператора удовлетворяет ||U|| ≤ 1.

LaTeX

$$$\\\\|U\\\\| \\\\le 1$$$

Lean4

/-- The entrywise sup norm of a unitary matrix is at most 1. -/
theorem entrywise_sup_norm_bound_of_unitary {U : Matrix n n 𝕜} (hU : U ∈ Matrix.unitaryGroup n 𝕜) : ‖U‖ ≤ 1 :=
  by
  simp_rw [pi_norm_le_iff_of_nonneg zero_le_one]
  intros
  exact entry_norm_bound_of_unitary hU _ _

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