Symmetric Invertible Approximation of a Symmetric Matrix

This is a finite-dimensional matrix approximation lemma.

Let $\iota$ be a finite type with decidable equality, and let $A$ be a real $\iota\times\iota$ matrix satisfying $A^{\mathsf T}=A$. Then there exists a sequence of matrices $(A_k)_{k\in\mathbb N}$ such that every $A_k$ is symmetric and invertible, and

as $k\to\infty$ in the matrix topology. The result supplies invertible symmetric approximants without requiring $A$ itself to be invertible.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

set_option maxHeartbeats 300000 in
theorem exists_symmetric_isUnit_matrix_sequence {ι : Type*} [Fintype ι] [DecidableEq ι]
    (A : Matrix ι ι ℝ) (hA : A.IsSymm) :
    ∃ seq : ℕ → Matrix ι ι ℝ,
      (∀ k, (seq k).IsSymm ∧ IsUnit (seq k)) ∧ Tendsto seq atTop (𝓝 A)

Module navigation

Module: Analysis/Matrix/Sign.

Previous: symmetric_matrix_spectral_geometry.

Source excerpt, lines 416–420 · Frozen source 408915f.