LinearMap.IsSymmetric.eigenvalues has all the eigenvalues

Stream: Is there code for X?

[Niels Voss]

docs#LinearMap.IsSymmetric.hasEigenvalue_eigenvalues states that all elements of the form hT.eigenvalues hn i are actually eigenvalues of T. Is there a theorem for the converse, which is that all the eigenvalues actually appear in LinearMap.IsSymmetric.eigenvalues?

lemma IsSymmetric.exists_eigenvalues_eq {T : Module.End 𝕜 E} (hT : T.IsSymmetric) {n : ℕ}
  (hn : Module.finrank 𝕜 E = n) {μ : 𝕜} (hμ : T.HasEigenvalue μ)
  : ∃ i : Fin n, hT.eigenvalues hn i = μ := by
  sorry

[Jireh Loreaux]

docs#LinearMap.IsSymmetric.diagonalization_apply_self_apply

[Jireh Loreaux]

Hmmm... maybe that's not quite what we're going for.

[Aaron Liu]

Jireh Loreaux said:

docs#LinearMap.IsSymmetric.diagonalization_apply_self_apply

something's wrong with the pretty printing for docs#Module.End.UnifEigenvalues.val

[Jireh Loreaux]

There are some issues here. This unsortedEigenvalues is marked private but I don't think it should be.

[Jireh Loreaux]

That's why we have some set_option back.privateInPublics later down the file.

[Jireh Loreaux]

Yeah, unfortunately we don't have it. You'll have to get into the weeds of docs#DirectSum.IsInternal.subordinateOrthonormalBasis.

[Niels Voss]

Would this be something we want in mathlib?

[Niels Voss]

I managed to prove the unsortedEigenvalues version in a few short lemmas by dealing with the subordinateOrthonormalBasis weeds, and I think I can extend it to the eigenvalues. Does it make sense to have an alternative form for real numbers? Like

lemma IsSymmetric.exists_eigenvalues_eq' {T : Module.End 𝕜 E} (hT : T.IsSymmetric) {n : ℕ}
  (hn : Module.finrank 𝕜 E = n) {μ : ℝ} (hμ : T.HasEigenvalue μ)
  : ∃ i : Fin n, hT.eigenvalues hn i = μ := by
  sorry

because giving a μ : ℝ into the one expecting μ : 𝕜 will produce a proof of something like ∃ i : Fin n, ofReal (hT.eigenvalues hn i) = ofReal μ, which is inefficient?

[Edison Xie]

import Mathlib

theorem IsSymmetric.mem_range_eigenvalues {𝕜 E : Type*} [RCLike 𝕜] {n} [NormedAddCommGroup E]
    [InnerProductSpace 𝕜 E] (hn : Module.finrank 𝕜 E = n) [FiniteDimensional 𝕜 E]
    {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (μ : 𝕜) (hμ : Module.End.HasEigenvalue T μ) :
    ∃ i, hT.eigenvalues hn i = μ := by
  obtain ⟨v, hv_mem, hv_ne⟩ := hμ.exists_hasEigenvector
  let B := hT.eigenvectorBasis hn
  have h_ne_zero : B.repr v ≠ 0 := fun h ↦ hv_ne <| B.repr.injective (map_zero B.repr ▸ h)
  obtain ⟨i, hi⟩ : ∃ i, B.repr v i ≠ 0 := by_contra fun h ↦ h_ne_zero <|
    PiLp.ext fun j ↦ (by simpa using h : ∀ j, (B.repr v).ofLp j = 0) j
  have h_diag := hT.eigenvectorBasis_apply_self_apply hn v i
  replace h_diag : μ = hT.eigenvalues hn i ∨ (B.repr v).ofLp i = 0 := by
    simpa [Module.End.mem_eigenspace_iff.1 hv_mem] using h_diag
  exact ⟨i, by simpa [hi, eq_comm] using h_diag⟩

if it helps

[Niels Voss]

That works; I was thinking we should probably have a lemma in Mathlib/Analysis/InnerProductSpace/PiL2.lean which states

theorem DirectSum.IsInternal.exists_subordinateOrthonormalBasisIndex_eq
    (hV' : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ)
    {i : ι} (hi : V i ≠ ⊥) :
    ∃ a : Fin n, i = hV.subordinateOrthonormalBasisIndex hn a hV' := by
  have : 0 < finrank 𝕜 (V i) := by rwa [←Nat.ne_zero_iff_zero_lt, finrank_eq_zero.ne]
  use hV.sigmaOrthonormalBasisIndexEquiv hn hV' ⟨i, ⟨0, this⟩⟩
  simp [DirectSum.IsInternal.subordinateOrthonormalBasisIndex_def]

which eventually leads to the desired theorem, and is somewhat more direct than using the eigenbasis (although the total proof will probably be a bit longer).

[Niels Voss]

I finished the proof. I've opened #34362 because I heard that PRs are easier to review than Zulip messages; if Edison Xie's proof is preferred to mine, feel free to close the PR and open a different one.

[Niels Voss]

Unfortunately, I discovered that for #33731, I actually need the stronger statement

theorem card_filter_eigenvalues_eq (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {μ : 𝕜}
    (hμ : HasEigenvalue T μ) : Finset.card {i : Fin n | hT.eigenvalues hn i = μ}
      = Module.finrank 𝕜 (Module.End.eigenspace T μ) := by

which I am almost done proving. I will probably open a PR for this once I finish.
Hopefully, it will be independent of #34362 (I could use these lemmas to simplify the proofs in #34362, but they won't simplify that much, if at all, so I don't think it's worth the extra sophistication).

[Niels Voss]

In the meantime, does anyone have any suggestions on how to simplify this proof?

-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
private def DirectSum.IsInternal.subordinateOrthonormalBasisIndexFiberEquiv
    (hV' : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) (i : ι) :
    {a : Fin n // hV.subordinateOrthonormalBasisIndex hn a hV' = i} ≃ Fin (finrank 𝕜 (V i)) where
  toFun a := Fin.cast (by rw [←subordinateOrthonormalBasisIndex_def, a.property])
    ((hV.sigmaOrthonormalBasisIndexEquiv hn hV').symm a).snd
  invFun b := ⟨hV.sigmaOrthonormalBasisIndexEquiv hn hV' ⟨i, b⟩,
    by simp [subordinateOrthonormalBasisIndex_def]⟩
  left_inv := by
    intro ⟨a, ha⟩
    rw [subordinateOrthonormalBasisIndex_def] at ha
    rw! [←ha]
    simp
  right_inv b := by
    ext
    dsimp only [Fin.val_cast]
    rw [Equiv.symm_apply_apply]

theorem DirectSum.IsInternal.card_filter_subordinateOrthonormalBasisIndex_eq
    (hV' : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) (i : ι) :
    Finset.card {a : Fin n | hV.subordinateOrthonormalBasisIndex hn a hV' = i}
    = finrank 𝕜 (V i) := by
  apply Finset.card_eq_of_equiv_fin
  simpa using hV.subordinateOrthonormalBasisIndexFiberEquiv hn hV'

I think the rw! tactic saved me quite a few hours and many lines of code, but ideally I would like to avoid getting into a dependent type mess in the first place.

[Vlad Tsyrklevich]

Could you make it an #mwe?

[Niels Voss]

module

public import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Tactic.DepRewrite

open Module Real Set Filter RCLike Submodule Function Uniformity Topology NNReal ENNReal
  ComplexConjugate DirectSum WithLp

noncomputable section

variable {ι 𝕜 : Type*} [RCLike 𝕜] {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E]
variable {n : ℕ} (hn : finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V)

private def DirectSum.IsInternal.subordinateOrthonormalBasisIndexFiberEquiv
    (hV' : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) (i : ι) :
    {a : Fin n // hV.subordinateOrthonormalBasisIndex hn a hV' = i} ≃ Fin (finrank 𝕜 (V i)) where
  toFun a := Fin.cast (by rw [←subordinateOrthonormalBasisIndex_def, a.property])
    ((hV.sigmaOrthonormalBasisIndexEquiv hn hV').symm a).snd
  invFun b := ⟨hV.sigmaOrthonormalBasisIndexEquiv hn hV' ⟨i, b⟩,
    by simp [subordinateOrthonormalBasisIndex_def]⟩
  left_inv := by
    intro ⟨a, ha⟩
    rw [subordinateOrthonormalBasisIndex_def] at ha
    rw! [←ha]
    simp
  right_inv b := by
    ext
    dsimp only [Fin.val_cast]
    rw [Equiv.symm_apply_apply]

theorem DirectSum.IsInternal.card_filter_subordinateOrthonormalBasisIndex_eq
    (hV' : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) (i : ι) :
    Finset.card {a : Fin n | hV.subordinateOrthonormalBasisIndex hn a hV' = i}
    = finrank 𝕜 (V i) := by
  apply Finset.card_eq_of_equiv_fin
  simpa using hV.subordinateOrthonormalBasisIndexFiberEquiv hn hV' i

For some extra context:

• hV.subordinateOrthonormalBasisIndex hn · hV' is a function Fin n → ι defined by hV.subordinateOrthonormalBasisIndex hn a hV' = ((hV.sigmaOrthonormalBasisIndexEquiv hn hV').symm a).1
• hV.sigmaOrthonormalBasisIndexEquiv hn hV' is effectively an opaque equivalence (i : ι) × Fin (finrank 𝕜 ↥(V i)) ≃ Fin n (note the dependent sum type).
• If we abbreviate these as sOBI and sOBIE, and if the equivalence I am defining is f, then $f(a) = \pi_2(\text{sOBIE}(a))$ and $f^{-1}(b) = \text{sOBIE}((i,b))$

[Niels Voss]

I opened #34660 with this new proof