[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ‖U i j‖ ≤ 1
[PROOFSTEP]
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 
    cases' h_x with a h_a
    rw [← h_a.2]
    apply sq_nonneg
  · rw [Multiset.mem_map]
    use j
    simp only [eq_self_iff_true, Finset.mem_univ_val, and_self_iff, sq_eq_sq]
      -- The L2 norm of a row is a diagonal entry of U * Uᴴ
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
[PROOFSTEP]
apply Multiset.single_le_sum
[GOAL]
case a
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ∀ (x : ℝ), x ∈ Multiset.map (fun x => ‖U i x‖ ^ 2) Finset.univ.val → 0 ≤ x
[PROOFSTEP]
intro x h_x
[GOAL]
case a
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
h_x : x ∈ Multiset.map (fun x => ‖U i x‖ ^ 2) Finset.univ.val
⊢ 0 ≤ x
[PROOFSTEP]
rw [Multiset.mem_map] at h_x 
[GOAL]
case a
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
h_x : ∃ a, a ∈ Finset.univ.val ∧ ‖U i a‖ ^ 2 = x
⊢ 0 ≤ x
[PROOFSTEP]
cases' h_x with a h_a
[GOAL]
case a.intro
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
a : n
h_a : a ∈ Finset.univ.val ∧ ‖U i a‖ ^ 2 = x
⊢ 0 ≤ x
[PROOFSTEP]
rw [← h_a.2]
[GOAL]
case a.intro
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
a : n
h_a : a ∈ Finset.univ.val ∧ ‖U i a‖ ^ 2 = x
⊢ 0 ≤ ‖U i a‖ ^ 2
[PROOFSTEP]
apply sq_nonneg
[GOAL]
case a
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ‖U i j‖ ^ 2 ∈ Multiset.map (fun x => ‖U i x‖ ^ 2) Finset.univ.val
[PROOFSTEP]
rw [Multiset.mem_map]
[GOAL]
case a
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ∃ a, a ∈ Finset.univ.val ∧ ‖U i a‖ ^ 2 = ‖U i j‖ ^ 2
[PROOFSTEP]
use j
[GOAL]
case h
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ j ∈ Finset.univ.val ∧ ‖U i j‖ ^ 2 = ‖U i j‖ ^ 2
[PROOFSTEP]
simp only [eq_self_iff_true, Finset.mem_univ_val, and_self_iff, sq_eq_sq]
  -- The L2 norm of a row is a diagonal entry of U * Uᴴ
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
⊢ ‖U i j‖ ≤ 1
[PROOFSTEP]
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, IsROrC.mul_conj, IsROrC.normSq_eq_def',
    IsROrC.ofReal_pow];
  norm_cast
    -- The L2 norm of a row is a diagonal entry of U * Uᴴ, real part
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
⊢ (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
[PROOFSTEP]
simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, ← starRingEnd_apply, IsROrC.mul_conj, IsROrC.normSq_eq_def',
  IsROrC.ofReal_pow]
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
⊢ ∑ x : n, ↑‖U i x‖ ^ 2 = ↑(∑ x : n, ‖U i x‖ ^ 2)
[PROOFSTEP]
norm_cast
  -- The L2 norm of a row is a diagonal entry of U * Uᴴ, real part
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
⊢ ‖U i j‖ ≤ 1
[PROOFSTEP]
have re_diag_eq_norm_sum : IsROrC.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2 :=
  by
  rw [IsROrC.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
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
⊢ ↑IsROrC.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2
[PROOFSTEP]
rw [IsROrC.ext_iff] at diag_eq_norm_sum 
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum✝ : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
diag_eq_norm_sum :
  ↑IsROrC.re ((U * Uᴴ) i i) = ↑IsROrC.re ↑(∑ x : n, ‖U i x‖ ^ 2) ∧
    ↑IsROrC.im ((U * Uᴴ) i i) = ↑IsROrC.im ↑(∑ x : n, ‖U i x‖ ^ 2)
⊢ ↑IsROrC.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2
[PROOFSTEP]
rw [diag_eq_norm_sum.1]
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum✝ : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
diag_eq_norm_sum :
  ↑IsROrC.re ((U * Uᴴ) i i) = ↑IsROrC.re ↑(∑ x : n, ‖U i x‖ ^ 2) ∧
    ↑IsROrC.im ((U * Uᴴ) i i) = ↑IsROrC.im ↑(∑ x : n, ‖U i x‖ ^ 2)
⊢ ↑IsROrC.re ↑(∑ x : n, ‖U i x‖ ^ 2) = ∑ x : n, ‖U i x‖ ^ 2
[PROOFSTEP]
norm_cast
  -- Since U is unitary, the diagonal entries of U * Uᴴ are all 1
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : ↑IsROrC.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2
⊢ ‖U i j‖ ≤ 1
[PROOFSTEP]
have mul_eq_one : U * Uᴴ = 1 := unitary.mul_star_self_of_mem hU
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : ↑IsROrC.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2
mul_eq_one : U * Uᴴ = 1
⊢ ‖U i j‖ ≤ 1
[PROOFSTEP]
have diag_eq_one : IsROrC.re ((U * Uᴴ) i i) = 1 := by
  simp only [mul_eq_one, eq_self_iff_true, Matrix.one_apply_eq, IsROrC.one_re]
    -- Putting it all together
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : ↑IsROrC.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2
mul_eq_one : U * Uᴴ = 1
⊢ ↑IsROrC.re ((U * Uᴴ) i i) = 1
[PROOFSTEP]
simp only [mul_eq_one, eq_self_iff_true, Matrix.one_apply_eq, IsROrC.one_re]
  -- Putting it all together
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : ↑IsROrC.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2
mul_eq_one : U * Uᴴ = 1
diag_eq_one : ↑IsROrC.re ((U * Uᴴ) i i) = 1
⊢ ‖U i j‖ ≤ 1
[PROOFSTEP]
rw [← sq_le_one_iff (norm_nonneg (U i j)), ← diag_eq_one, re_diag_eq_norm_sum]
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : ↑IsROrC.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2
mul_eq_one : U * Uᴴ = 1
diag_eq_one : ↑IsROrC.re ((U * Uᴴ) i i) = 1
⊢ ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
[PROOFSTEP]
exact norm_sum
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
⊢ ‖U‖ ≤ 1
[PROOFSTEP]
conv =>
  -- Porting note: was `simp_rw [pi_norm_le_iff_of_nonneg zero_le_one]`
  rw [pi_norm_le_iff_of_nonneg zero_le_one]
  intro
  rw [pi_norm_le_iff_of_nonneg zero_le_one]
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
| ‖U‖ ≤ 1
[PROOFSTEP]
  rw [pi_norm_le_iff_of_nonneg zero_le_one]
  intro
  rw [pi_norm_le_iff_of_nonneg zero_le_one]
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
| ‖U‖ ≤ 1
[PROOFSTEP]
  rw [pi_norm_le_iff_of_nonneg zero_le_one]
  intro
  rw [pi_norm_le_iff_of_nonneg zero_le_one]
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
| ‖U‖ ≤ 1
[PROOFSTEP]
rw [pi_norm_le_iff_of_nonneg zero_le_one]
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
| ∀ (i : n), ‖U i‖ ≤ 1
[PROOFSTEP]
intro
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i✝ : n
| ‖U i✝‖ ≤ 1
[PROOFSTEP]
rw [pi_norm_le_iff_of_nonneg zero_le_one]
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
⊢ ∀ (i i_1 : n), ‖U i i_1‖ ≤ 1
[PROOFSTEP]
intros
[GOAL]
𝕜 : Type u_1
m : Type u_2
n : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i✝¹ i✝ : n
⊢ ‖U i✝¹ i✝‖ ≤ 1
[PROOFSTEP]
exact entry_norm_bound_of_unitary hU _ _
