A theorem about 2-Norm on Matrices

Stream: maths

[Hououin Kyouma]

I’m trying to prove the theorem below. So far, I’ve proven that matrix B is a Hermitian matrix, found its maximum eigenvalue and the corresponding eigenvector, and also shown that the norm of this eigenvector is 1. Now, there’s just one final step left: proving that λₘₐₓ = ||A||₂². How to approach this proof? (Some of the imports may be useless) Sorry, I've editted the message to make it readable.

import Mathlib.Analysis.InnerProductSpace.Spectrum
import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic
import Mathlib.LinearAlgebra.Matrix.Spectrum
import Mathlib.LinearAlgebra.Matrix.Symmetric
import Mathlib.LinearAlgebra.Matrix.Hermitian
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Fintype.Defs
import Mathlib.Data.Finset.Sups
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.LinearAlgebra.Matrix.ToLin
import Mathlib.Data.Matrix.Mul

noncomputable section

variable {𝕜 : Type*} [RCLike 𝕜]
variable {m n : Type*} [Fintype m] [Fintype n] [DecidableEq n]

def Matrix.norm₂ (A : Matrix m n 𝕜) : ℝ :=
  ‖(Matrix.toEuclideanLin A).toContinuousLinearMap‖

theorem Matrix.norm₂_eq_sSup_norm_on_sphere (A : Matrix m n 𝕜) :
  A.norm₂ = sSup ((fun x ↦ ‖(Matrix.toEuclideanLin A).toContinuousLinearMap x‖) '' {x : EuclideanSpace 𝕜 n | ‖x‖ = 1}) := by

  unfold Matrix.norm₂
  rw [← ContinuousLinearMap.sSup_sphere_eq_norm]

  have h_sets_eq : Metric.sphere (0 : EuclideanSpace 𝕜 n) 1 = {x | ‖x‖ = 1} := by
    ext x
    simp
  rw [h_sets_eq]
end

open Matrix
variable {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
variable [NormedAddCommGroup (Matrix m n ℝ)] [NormedSpace ℝ (Matrix m n ℝ)]
variable {A : Matrix m n ℝ}

theorem exists_unit_eigenvector_for_AT_A_of_norm_sq (hA : Nonempty n) :
  ∃ (z : EuclideanSpace ℝ n), ‖z‖ = 1 ∧ ((A.transpose * A) *ᵥ z = (A.norm₂ ^ 2) • z) := by

  let B := A.transpose * A
  have hB_herm : (A.transpose * A).IsHermitian := by
   rw [← conjTranspose_eq_transpose_of_trivial (A := A)]
   exact isHermitian_transpose_mul_self A

  have h_univ_nonempty : (Finset.univ : Finset n).Nonempty := by
    by_contra h_univ_is_empty
    rw [Finset.not_nonempty_iff_eq_empty] at h_univ_is_empty
    have is_empty_n : IsEmpty n := Finset.univ_eq_empty_iff.mp h_univ_is_empty
    exact is_empty_n.false (Nonempty.some hA)

  let evals : n → ℝ := hB_herm.eigenvalues

  let lambda_max := Finset.sup' Finset.univ h_univ_nonempty evals

  have h_exists_max_idx : ∃ j, j ∈ Finset.univ ∧ lambda_max = evals j :=
    Finset.exists_mem_eq_sup' h_univ_nonempty evals

  obtain ⟨j, _, h_j_is_max⟩ := h_exists_max_idx

  let z : EuclideanSpace ℝ n := hB_herm.eigenvectorBasis j

  have hz_norm : ‖z‖ = 1 :=
    hB_herm.eigenvectorBasis.orthonormal.norm_eq_one j

  have hz_eigenvector : B *ᵥ z = lambda_max • z := by

    rw [h_j_is_max]
    unfold B z
    exact hB_herm.mulVec_eigenvectorBasis j

  have h_lambda_eq_norm_sq : lambda_max = A.norm₂ ^ 2 := by

    sorry

  use z
  constructor
  · exact hz_norm
  · rw [hz_eigenvector, h_lambda_eq_norm_sq]

[Kevin Buzzard]

Please read #backticks and edit your message (don't post a new one, edit the old one) (hint: you're using the wrong character, it's ` not ' ) (PS: thanks! Looks much better now!)

[Eric Wieser]

You might be after docs#Matrix.toEuclideanCLM to make things a bit shorter

[Hououin Kyouma]

Eric Wieser said:

You might be after docs#Matrix.toEuclideanCLM to make things a bit shorter

I'm sorry but I don't know how to use it in my proof. :sob:

[Eric Wieser]

(Matrix.toEuclideanLin A).toContinuousLinearMap is a.toEuclideanCLM

[Jireh Loreaux]

You should be able to open the Matrix.Norm.L2Operator scope and then use docs#IsometricContinuousFunctionalCalculus.isGreatest_spectrum (with a := A.transpose * A, you may have to prove ha manually), to get that ‖A.transpose * A‖ is in the spectrum, from which you can then get that this is an eigenvalue with docs#Module.End.HasEigenvalue.of_mem_spectrum, from which you can get an eigenvector.