Formalize with Chebyshev polynomial.

Stream: new members

[Nick_adfor]

Problem: Let $n \times n$ matrix $A = \left( \begin{matrix} 0 & 1 & & & \\ 1 & 0 & 1 & & \\ & 1 & 0 & \ddots & \\ & & \ddots & \ddots & 1 \\ & & & 1 & 0 \end{matrix} \right)$. Prove that all eigenvalues of $A$ are real numbers and are pairwise distinct. (Hint: Consider the symmetry of the matrix and properties of the characteristic polynomial.)
Proof:
Let $A_n$ denote the $n \times n$ tridiagonal matrix in the problem (with 0 on the diagonal and 1 on the subdiagonal and superdiagonal). We want to prove that the eigenvalues of $A_n$ (counting algebraic multiplicity) are all real and distinct.

1. $A_n$ is a real symmetric matrix. Symmetric matrices are Hermitian, and Hermitian matrices have all real eigenvalues. Therefore, all eigenvalues are real.

2. Let $p_k(x) = \det(xI_k - A_k)$ (where $A_k$ is the $k \times k$ leading principal submatrix of $A_n$). We proceed by induction on $k$, expanding the determinant along the last row. Note that the last row of $xI_k - A_k$ has only two non-zero entries: the $k$-th column is $x$, the $(k-1)$-th column is $-1$, and all other entries are 0 (since the matrix has 1s only on the subdiagonal and superdiagonal). Therefore, expanding along the last row gives
   $p_k(x) = x \cdot p_{k-1}(x) - 1 \cdot p_{k-2}(x), \qquad p_0(x) = 1, \ p_1(x) = x.$
   This is a second-order linear recurrence relation with constant coefficients.

3. The Chebyshev polynomials of the second kind $U_k(t)$ are defined as
   $U_0(t) = 1, \quad U_1(t) = 2t, \quad U_{k+1}(t) = 2t \, U_k(t) - U_{k-1}(t).$
   Let $t = x/2$, then we have
   $U_0(x/2) = 1, \quad U_1(x/2) = x, \quad U_{k+1}(x/2) = x \, U_k(x/2) - U_{k-1}(x/2).$
   This matches the initial values and recurrence of $p_k$, so by induction $p_k(x) = U_k(x/2)$ holds for all $k$. Therefore,
   $\operatorname{charpoly}(A_n)(x) = p_n(x) = U_n(x/2).$

4. Regarding the zeros of $U_n$, there is a classical trigonometric representation: when $t = \cos\theta$,
   $U_n(\cos\theta) = \frac{\sin((n+1)\theta)}{\sin\theta}.$
   Therefore, the solutions to $U_n(t) = 0$ are exactly
   $t = \cos\frac{j\pi}{n+1}, \qquad j = 1, 2, \dots, n,$
   and each root is simple (because at these values of $\theta$, the numerator $\sin((n+1)\theta)$ has a simple zero while the denominator is non-zero). Therefore, the solutions to $p_n(x) = 0$ are
   $x = 2\cos\frac{j\pi}{n+1}, \qquad j = 1, 2, \dots, n,$
   and each root is simple, hence they are all distinct.
   In conclusion: All eigenvalues of $A_n$ are real and pairwise distinct (explicitly given by the formula above). This completes the proof.

[Nick_adfor]

(deleted)

[Nick_adfor]

@Weiyi Wang , I haven’t finished formatting yet, please wait a moment.

[Nick_adfor]

Lemma A (A is symmetric)
↓
Lemma B (symmetric ⇒ Hermitian ⇒ eigenvalues are real)
↓
Lemma C (characteristic polynomial recurrence p_k)
↓
Lemma D (Chebyshev U recurrence) → Lemma E (charpoly = U_n(x/2))
↓
Lemma F (roots of U_n are explicit and simple, choose path F1 or F2)
↓
Theorem 2 (roots are distinct)
↑
Theorem 1 (reality follows from Lemma B or directly from explicit roots)

[Weiyi Wang]

I mean this is a nice problem and proof, but I am not sure what to discuss here. Are you seeking translating this to Lean, or having difficulty finding specific theorem/definition?

[Nick_adfor]

import Mathlib

open Matrix Polynomial


variable (n : ℕ)

variable {R : Type*} [CommRing R]
open Polynomial Polynomial.Chebyshev

def A (n : ℕ) : Matrix (Fin n) (Fin n) ℝ :=
  Matrix.of fun i j =>
    if i = j then 0
    else if |(i : ℤ) - (j : ℤ)| = 1 then 1
    else 0

lemma A_symmetric (n : ℕ) : (A n).IsSymm :=
by
  unfold A Matrix.IsSymm
  sorry

lemma A_isHermitian (n : ℕ) : (A n).IsHermitian := by
  sorry

lemma charpoly_recursion :
  ∀ n, n ≥ 2 → (A n).charpoly = X * (A (n-1)).charpoly - (A (n-2)).charpoly := by
  sorry

lemma Chebyshev_U_recursion :
  ∀ n : ℕ, n ≥ 2 → Chebyshev.U ℝ n = 2 * X * Chebyshev.U ℝ (n-1) - Chebyshev.U ℝ (n-2) := by
  sorry

lemma charpoly_A_eq_ChebyshevU (n : ℕ) :
  (A n).charpoly = (Chebyshev.U ℝ n).comp (X / 2) := by
  sorry

noncomputable def eigenvalues (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) : Finset ℝ :=
  M.charpoly.roots.toFinset

lemma Chebyshev_U_simple_roots (n : ℕ) (x : ℝ) :
  ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 →
  ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval x ≠ 0 :=
sorry

theorem A_n_eigenvalues_real (n : ℕ) (χ : ℝ) (h : χ ∈ eigenvalues n (A n)) : χ ∈ ℝ := by sorry

theorem A_n_eigenvalues_distinct (n : ℕ) :
 (eigenvalues n (A n)).val.Nodup := by sorry

[Nick_adfor]

Weiyi Wang said:

I mean this is a nice problem and proof, but I am not sure what to discuss here. Are you seeking translating this to Lean, or having difficulty finding specific theorem/definition?

I'm sorry that I haven't given the lean code timely

[Nick_adfor]

I'm seeking translating this to Lean, and having difficulty for the penultimate theorem statement.

[Lawrence Wu (llllvvuu)]

χ ∈ ℝ isn't a proposition in Lean; Lean is based on type theory. Indeed you have already defined χ : ℝ so there is nothing to prove here.

[Nick_adfor]

Now this

import Mathlib

open Matrix Polynomial
open Polynomial Polynomial.Chebyshev

variable (n : ℕ)
variable {R : Type*} [CommRing R]

def A (n : ℕ) : Matrix (Fin n) (Fin n) ℝ :=
  Matrix.of fun i j =>
    if i = j then 0
    else if |(i : ℤ) - (j : ℤ)| = 1 then 1
    else 0

noncomputable def eigenvalues (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) : Finset ℝ :=
  M.charpoly.roots.toFinset

noncomputable def eigenvaluesC (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) : Finset ℂ :=
  ((M.map (algebraMap ℝ ℂ)).charpoly).roots.toFinset

lemma A_symmetric (n : ℕ) : (A n).IsSymm :=
by
  unfold A Matrix.IsSymm
  sorry

lemma A_map_isHermitian (n : ℕ) : ((A n).map (algebraMap ℝ ℂ)).IsHermitian := by
  have h_symm : (A n).IsSymm := A_symmetric n
  have : (A n).map (algebraMap ℝ ℂ) = (A n).map (algebraMap ℝ ℂ) := rfl
  have h_symm_map : (A n).map (algebraMap ℝ ℂ) = (A n).map (algebraMap ℝ ℂ) := rfl
  rw [this]
  sorry

lemma charpoly_recursion :
  ∀ n, n ≥ 2 → (A n).charpoly = X * (A (n-1)).charpoly - (A (n-2)).charpoly := by
  sorry

lemma Chebyshev_U_recursion :
  ∀ n : ℕ, n ≥ 2 → Chebyshev.U ℝ n = 2 * X * Chebyshev.U ℝ (n-1) - Chebyshev.U ℝ (n-2) := by
  sorry

lemma charpoly_A_eq_ChebyshevU (n : ℕ) :
  (A n).charpoly = (Chebyshev.U ℝ n).comp (X / 2) := by
  sorry

lemma Chebyshev_U_simple_roots (n : ℕ) (x : ℝ) :
  ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 →
  ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval x ≠ 0 := by
sorry

theorem A_n_eigenvalues_real_C (n : ℕ) :
  ∀ (ζ : ℂ), ζ ∈ eigenvaluesC n (A n) → ∃ (r : ℝ), ζ = (algebraMap ℝ ℂ) r := by
  intro ζ hζ
  let M := (A n).map (algebraMap ℝ ℂ)
  have hM : M.IsHermitian := A_map_isHermitian n
  sorry

theorem A_n_eigenvalues_distinct (n : ℕ) :
 (eigenvalues n (A n)).val.Nodup := by sorry

[Nick_adfor]

[ A_symmetric ] ───▶ [ A_map_isHermitian ] ───▶ [ A_n_eigenvalues_real_C ]

[ charpoly_recursion ] ─┐
                        ├──▶ [ charpoly_A_eq_ChebyshevU ] ─┐
[ Chebyshev_U_recursion ] ┘                               │
                                                          ├──▶ [ A_n_eigenvalues_distinct ]
[ Chebyshev_U_simple_roots ] ─────────────────────────────┘

[Nick_adfor]

Now this.

import Mathlib

open Matrix Polynomial
open Polynomial Polynomial.Chebyshev

variable (n : ℕ)
variable {R : Type*} [CommRing R]

def A (n : ℕ) : Matrix (Fin n) (Fin n) ℝ :=
  Matrix.of fun i j =>
    if i = j then 0
    else if |(i : ℤ) - (j : ℤ)| = 1 then 1
    else 0

noncomputable def eigenvalues (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) : Finset ℝ :=
  M.charpoly.roots.toFinset

noncomputable def eigenvaluesC (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) : Finset ℂ :=
  ((M.map (algebraMap ℝ ℂ)).charpoly).roots.toFinset

lemma A_symmetric (n : ℕ) : (A n).IsSymm := by
  unfold A Matrix.IsSymm
  ext i j
  simp only [Matrix.transpose_apply]
  by_cases h : i = j
  · simp only [h, of_apply, ↓reduceIte]
  · by_cases h_adj : |(i : ℤ) - (j : ℤ)| = 1
    · have h_swap : |(j : ℤ) - (i : ℤ)| = 1 := by
        rw [abs_sub_comm]
        exact h_adj
      simp only [of_apply, ne_comm.mp h, ↓reduceIte, h_swap, h, h_adj]
    · have h_not_swap : ¬(|(j : ℤ) - (i : ℤ)| = 1) := by
        rw [abs_sub_comm]
        exact h_adj
      simp only [of_apply, ne_comm.mp h, ↓reduceIte, h_not_swap, h, h_adj]

lemma A_map_isHermitian (n : ℕ) : ((A n).map (algebraMap ℝ ℂ)).IsHermitian := by
  have h_symm : (A n).IsSymm := A_symmetric n
  unfold Matrix.IsHermitian
  ext i j
  simp only [Complex.coe_algebraMap, conjTranspose_apply, map_apply, RCLike.star_def, Complex.conj_ofReal, Complex.ofReal_inj]
  rw [Matrix.IsSymm] at h_symm
  exact congrFun (congrFun (id (Eq.symm h_symm)) j) i

lemma charpoly_recursion :
  ∀ k, k ≥ 2 → (A k).charpoly = X * (A (k-1)).charpoly - (A (k-2)).charpoly := by
  sorry

lemma Chebyshev_U_recursion :
  ∀ n : ℕ, n ≥ 2 → Chebyshev.U ℝ n = 2 * X * Chebyshev.U ℝ (n-1) - Chebyshev.U ℝ (n-2) := by
  sorry

lemma charpoly_A_eq_ChebyshevU (n : ℕ) :
  (A n).charpoly = (Chebyshev.U ℝ n).comp (X / 2) := by
  sorry

lemma Chebyshev_U_simple_roots (n : ℕ) (x : ℝ) :
  ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 →
  ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval x ≠ 0 := by
sorry

theorem A_n_eigenvalues_real_C (n : ℕ) :
  ∀ (ζ : ℂ), ζ ∈ eigenvaluesC n (A n) → ∃ (r : ℝ), ζ = (algebraMap ℝ ℂ) r := by
  intro ζ hζ
  let M := (A n).map (algebraMap ℝ ℂ)
  have hM : M.IsHermitian := A_map_isHermitian n
  sorry

theorem A_n_eigenvalues_distinct (n : ℕ) :
 (eigenvalues n (A n)).val.Nodup := by sorry

[Lawrence Wu (llllvvuu)]

I made that connection here: #29476

[Nick_adfor]

For lemma charpoly_recursion, I decide to extract more lemma from it. Now I give a M_row_vals.

import Mathlib

open Matrix Polynomial
open Polynomial Polynomial.Chebyshev

variable (n : ℕ)
variable {R : Type*} [CommRing R]

def A (n : ℕ) : Matrix (Fin n) (Fin n) ℝ :=
  Matrix.of fun i j =>
    if i = j then 0
    else if |(i : ℤ) - (j : ℤ)| = 1 then 1
    else 0

noncomputable def eigenvalues (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) : Finset ℝ :=
  M.charpoly.roots.toFinset

noncomputable def eigenvaluesC (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) : Finset ℂ :=
  ((M.map (algebraMap ℝ ℂ)).charpoly).roots.toFinset

lemma A_symmetric (n : ℕ) : (A n).IsSymm := by
  unfold A Matrix.IsSymm
  ext i j
  simp only [Matrix.transpose_apply]
  by_cases h : i = j
  · simp only [h, of_apply, ↓reduceIte]
  · by_cases h_adj : |(i : ℤ) - (j : ℤ)| = 1
    · have h_swap : |(j : ℤ) - (i : ℤ)| = 1 := by
        rw [abs_sub_comm]
        exact h_adj
      simp only [of_apply, ne_comm.mp h, ↓reduceIte, h_swap, h, h_adj]
    · have h_not_swap : ¬(|(j : ℤ) - (i : ℤ)| = 1) := by
        rw [abs_sub_comm]
        exact h_adj
      simp only [of_apply, ne_comm.mp h, ↓reduceIte, h_not_swap, h, h_adj]

lemma A_map_isHermitian (n : ℕ) : ((A n).map (algebraMap ℝ ℂ)).IsHermitian := by
  have h_symm : (A n).IsSymm := A_symmetric n
  unfold Matrix.IsHermitian
  ext i j
  simp only [Complex.coe_algebraMap, conjTranspose_apply, map_apply, RCLike.star_def, Complex.conj_ofReal, Complex.ofReal_inj]
  rw [Matrix.IsSymm] at h_symm
  exact congrFun (congrFun (id (Eq.symm h_symm)) j) i

lemma M_row_vals (m : ℕ) (i : Fin (m + 2)) (ip : Fin (m + 2)) (h_ip_val : ip.val = m) (h_i_val : i.val = m + 1) :
    ∀ j : Fin (m + 2), (A (m + 2)).charmatrix i j =
      if j = i then Polynomial.X
      else if j = ip then Polynomial.C (-1)
      else 0 := by
    intro j
    have : (A (m + 2)).charmatrix = diagonal (fun _ : Fin (m + 2) => X) - (A (m + 2)).map C := rfl
    rw [this]
    simp only [Matrix.sub_apply, Matrix.diagonal_apply, Matrix.map_apply, map_neg, _root_.map_one]
    by_cases heq : j = i
    · simp only [heq, ↓reduceIte, sub_eq_self, map_eq_zero]
      have diag_zero : (A (m + 2)) i i = 0 := by
        unfold A
        simp only [of_apply, ↓reduceIte]
      simp only [diag_zero]
    · simp [heq]
      by_cases hprev : j = ip
      · simp only [hprev, ↓reduceIte]
        have adj_one : (A (m + 2)) i ip = 1 := by
          unfold A
          simp only [of_apply]
          rw [@ite_eq_iff]
          · simp only [zero_ne_one, and_false, ite_eq_left_iff, imp_false, Decidable.not_not,
            false_or]
            rw [← hprev]
            constructor
            · exact fun a => heq (id (Eq.symm a))
            · show |((i : ℤ) - (j : ℤ))| = 1
              have i_val : (i : ℤ) = (m + 1 : ℕ) := by
                simp only [Nat.cast_add, Nat.cast_one]
                exact congrArg Nat.cast h_i_val
              have ip_val : (j : ℤ) = (m : ℕ) := by
                simp only [Nat.cast_inj]
                rw [hprev, h_ip_val]
              rw [i_val, ip_val]
              norm_num
        rw [adj_one]
        simp only [_root_.map_one, sub_eq_neg_self, ite_eq_right_iff, X_ne_zero, imp_false, ne_eq,
          ]
        exact ne_of_ne_of_eq (fun a => heq (id (Eq.symm a))) hprev
      · simp [hprev]
        have zero_entry : (A (m + 2)) i j = 0 := by
          unfold A
          simp only [of_apply, ite_eq_left_iff, ite_eq_right_iff, one_ne_zero, imp_false]
          intro habs
          have : j.val ≤ m := by
            by_contra! H
            have : j.val = m + 1 := by
              have := j.2
              omega
            apply heq
            exact Fin.ext (show j.val = i.val from by rw [h_i_val, this])
          have i_val_eq : (i : ℤ) = (m + 1 : ℕ) := by
            simp only [Nat.cast_add, Nat.cast_one]
            exact congrArg Nat.cast h_i_val
          have j_val_eq : (j : ℤ) = (j.val : ℕ) := by
            simp only
          have ip_val_eq : (ip : ℤ) = (m : ℕ) := by
            simp only [Nat.cast_inj]
            rw [h_ip_val]
          have j_ne_ip_val : (j : ℤ) ≠ (ip : ℤ) := by
            intro h
            apply hprev
            exact Fin.ext (by
              exact Int.ofNat_inj.mp h
              )
          simp only [ip_val_eq, ne_eq, Nat.cast_inj] at j_ne_ip_val
          intro habs_abs
          have : |(m + 1 : ℤ) - (j.val : ℤ)| = 1 := by
            rw [show (i : ℤ) = (m + 1 : ℕ) from by simp [h_i_val]] at habs_abs
            exact habs_abs
          have : (m + 1 : ℤ) - (j.val : ℤ) = 1 ∨ (m + 1 : ℤ) - (j.val : ℤ) = -1 := by
            exact abs_eq_abs.mp this
          cases' this with h h
          · have h1 : (j.val : ℤ) = m := by omega
            have h2 : (j : ℤ) = m := by
              simp only [Nat.cast_inj]
              exact Eq.symm ((fun {m n} => Int.ofNat_inj.mp) (id (Eq.symm h1)))
            have h3 : (ip : ℤ) = m := by
              simp only [Nat.cast_inj]
              rw [h_ip_val]
            apply j_ne_ip_val
            exact Eq.symm ((fun {m n} => Int.ofNat_inj.mp) (id (Eq.symm h1)))
          · have : (j.val : ℤ) = m + 2 := by omega
            have : j.val ≤ m + 1 := by omega
            omega
        simp only [zero_entry, map_zero, sub_zero, ite_eq_right_iff, X_ne_zero, imp_false, ne_eq]
        exact fun a => heq (id (Eq.symm a))

lemma charpoly_recursion :
  ∀ k, k ≥ 2 → (A k).charpoly = X * (A (k-1)).charpoly - (A (k-2)).charpoly := by
  intro k hk
  obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le hk
  have hch : (A (m + 2)).charpoly = ((A (m + 2)).charmatrix).det := by
    simp only [charpoly]
  let M := (A (m + 2)).charmatrix
  have last_lt : m + 1 < m + 2 := by omega
  have prev_lt : m < m + 2 := by omega
  let i : Fin (m + 2) := ⟨m + 1, last_lt⟩
  let ip : Fin (m + 2) := ⟨m, prev_lt⟩
  have M_row_vals : ∀ j : Fin (m + 2), M i j =
      if j = i then Polynomial.X
      else if j = ip then Polynomial.C (-1)
      else 0 := by exact fun j => M_row_vals m i ip rfl rfl j
  -- 2) Use Laplace expansion (expand along row i)
  --    Matrix.det (M) = ∑_{j : Fin k} (-1)^(i+j) * M i j * (M.submatrix i j).det
  --    In mathlib4, available lemmas: `Matrix.det_succ_row` or `Matrix.det_expand_row` / expansion of `Matrix.det`
  have det_expansion := Matrix.det_succ_row M i
  -- det_expansion gives a sum over j (Finset.sum), below we filter out that only j = i and j = i.pred terms are non-zero
  -- 3) Use Finset.sum_eq_single twice to reduce the sum to two terms:
  --    First extract the j = i term from the sum, the rest are 0 (because M i j = 0)
  let S := Finset.univ.filter fun j => ¬ (j = i)  -- (backup)
  have only_two_nonzero : True := by
    -- Formalization steps (idea):
    -- (a) From det_expansion: M.det = ∑_{j} (-1)^(i+j) * M i j * ((M.submatrix ...).det)
    -- (b) For any j with j ≠ i and not (↑i = ↑j + 1) show M i j = 0 using M_row_vals
    -- (c) Apply `Finset.sum_eq_single` twice to extract the two non-zero indices j = i and j = i.pred
    -- Implementation details (TODO):
    --   use `Finset.sum_eq_single` with the index `j0 = i` then with `j1 = Fin.mk (i.val - 1) _`
    admit

  -- 4) Calculate the remaining two terms and identify the minors as determinants of smaller order charmatrices (i.e., charpoly of smaller A)
  --    Specifically: M.det = ( (-1)^(i+i) * M i i * det(M^{(i,i)}) ) +
  --                 ( (-1)^(i+i-1) * M i (i-1) * det(M^{(i,i-1)}) )
  --    Use M_row_vals to get M i i = X, M i (i-1) = C (-1), and note that (-1)^(2i) = 1, (-1)^(2i-1) = -1
  have minors_identified : True := by
    -- Need to prove:
    -- (M.submatrix i.succAbove i.succAbove).det = ((A (k-1)).charmatrix).det
    -- (M.submatrix i.succAbove (i.pred).succAbove).det = ((A (k-2)).charmatrix).det
    -- Proof method: Expand the definitions of submatrix and charmatrix, compare term by term (mechanical steps)
    admit

  -- 5) Substitute the above equations back, combining hch (and the same hch for smaller k) to get the final recursion
  --   i.e., (A k).charpoly = X * (A (k-1)).charpoly - (A (k-2)).charpoly
  have final_eq : (A (2 + m)).charpoly = X * (A (2 + m - 1)).charpoly - (A (2 + m - 2)).charpoly := by
    -- Construct the equation using hch, minors_identified, M_row_vals, det_expansion, only_two_nonzero
    admit
  exact final_eq

lemma Chebyshev_U_recursion :
  ∀ n : ℕ, n ≥ 2 → Chebyshev.U ℝ n = 2 * X * Chebyshev.U ℝ (n-1) - Chebyshev.U ℝ (n-2) := by
  sorry

lemma charpoly_A_eq_ChebyshevU (n : ℕ) :
  (A n).charpoly = (Chebyshev.U ℝ n).comp (X / 2) := by
  sorry

lemma Chebyshev_U_simple_roots (n : ℕ) (x : ℝ) :
  ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 →
  ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval x ≠ 0 := by
sorry

theorem A_n_eigenvalues_real_C (n : ℕ) :
  ∀ (ζ : ℂ), ζ ∈ eigenvaluesC n (A n) → ∃ (r : ℝ), ζ = (algebraMap ℝ ℂ) r := by
  intro ζ hζ
  let M := (A n).map (algebraMap ℝ ℂ)
  have hM : M.IsHermitian := A_map_isHermitian n
  sorry

theorem A_n_eigenvalues_distinct (n : ℕ) :
 (eigenvalues n (A n)).val.Nodup := by sorry