English
For a unitary matrix U, every entry has modulus at most 1: |U_{ij}| ≤ 1 for all i,j.
Русский
Для унитарной матрицы U каждый элемент удовлетворяет |U_{ij}| ≤ 1.
LaTeX
$$$|U_{ij}| \\\\le 1 \\\\quad \\text{for all } i,j$$$
Lean4
theorem entry_norm_bound_of_unitary {U : Matrix n n 𝕜} (hU : U ∈ Matrix.unitaryGroup n 𝕜) (i j : n) : ‖U i j‖ ≤ 1 := by
-- The norm squared of an entry is at most the L2 norm of its row.
have norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2 :=
by
apply Multiset.single_le_sum
· intro x h_x
rw [Multiset.mem_map] at h_x
obtain ⟨a, h_a⟩ := h_x
rw [← h_a.2]
apply sq_nonneg
· rw [Multiset.mem_map]
use j
simp only [Finset.mem_univ_val, and_self_iff]
-- The L2 norm of a row is a diagonal entry of U * Uᴴ
have diag_eq_norm_sum : (U * Uᴴ) i i = (∑ x : n, ‖U i x‖ ^ 2 : ℝ) :=
by
simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, ← starRingEnd_apply, RCLike.mul_conj]
norm_cast
-- The L2 norm of a row is a diagonal entry of U * Uᴴ, real part
have re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2 :=
by
rw [RCLike.ext_iff] at diag_eq_norm_sum
rw [diag_eq_norm_sum.1]
norm_cast
-- Since U is unitary, the diagonal entries of U * Uᴴ are all 1
have mul_eq_one : U * Uᴴ = 1 := unitary.mul_star_self_of_mem hU
have diag_eq_one : RCLike.re ((U * Uᴴ) i i) = 1 := by
simp only [mul_eq_one, Matrix.one_apply_eq, RCLike.one_re]
-- Putting it all together
rw [← sq_le_one_iff₀ (norm_nonneg (U i j)), ← diag_eq_one, re_diag_eq_norm_sum]
exact norm_sum
