English
Let A be a Hermitian matrix. There is a natural star-algebra homomorphism, called the continuous functional calculus, from the algebra of real-valued continuous functions on the spectrum of A into the algebra of n-by-n matrices, given by conjugating a real-diagonal function of the eigenvalues by the unitary of eigenvectors. Concretely, for g ∈ C(spectrumℝA, ℝ), the image is U diag(g(λ_i)) U*, where U is the eigenvector-unitary of A and λ_i are the eigenvalues.
Русский
Пусть A — эрмитова матрица. Существует естественный star-алгебра-однородный гомоморфизм, называемый непрерывным функциональным калькулятором, из алгебры вещественно-значных непрерывных функций на спектре A в матричную алгебру размерами n×n, заданный через преобразование по собственным векторам: для g ∈ C( SpectrumℝA, ℝ ) изображение равно U diag(g(λ_i)) U*, где U — матрица собственных векторов, а λ_i — собственные значения.
LaTeX
$$$cfcAux(g) = U \; \mathrm{diag}(g(\lambda_i)) \; U^*$, where $U = \text{eigenvectorUnitary}(A)$ and $\lambda_i$ are the eigenvalues of $A$.$$
Lean4
/-- The star algebra homomorphism underlying the instance of the continuous functional
calculus of a Hermitian matrix. This is an auxiliary definition and is not intended
for use outside of this file. -/
@[simps]
noncomputable def cfcAux : C(spectrum ℝ A, ℝ) →⋆ₐ[ℝ] (Matrix n n 𝕜)
where
toFun := fun g =>
(eigenvectorUnitary hA : Matrix n n 𝕜) *
diagonal (RCLike.ofReal ∘ g ∘ (fun i ↦ ⟨hA.eigenvalues i, hA.eigenvalues_mem_spectrum_real i⟩)) *
star (eigenvectorUnitary hA : Matrix n n 𝕜)
map_zero' := by simp [Pi.zero_def, Function.comp_def]
map_one' := by simp [Pi.one_def, Function.comp_def]
map_mul' f
g :=
by
have {a b c d e f : Matrix n n 𝕜} : (a * b * c) * (d * e * f) = a * (b * (c * d) * e) * f := by
simp only [mul_assoc]
simp only [this, ContinuousMap.coe_mul, SetLike.coe_mem, unitary.star_mul_self_of_mem, mul_one,
diagonal_mul_diagonal, Function.comp_apply]
congr! with i
simp
map_add' f
g := by
simp only [ContinuousMap.coe_add, ← add_mul, ← mul_add, diagonal_add, Function.comp_apply]
congr! with i
simp
commutes'
r := by
simp only [Function.comp_def, algebraMap_apply, smul_eq_mul, mul_one]
rw [← mul_one (algebraMap _ _ _), ← unitary.coe_mul_star_self hA.eigenvectorUnitary, ← Algebra.left_comm,
unitary.coe_star, mul_assoc]
congr!
map_star'
f :=
by
simp only [star_trivial, StarMul.star_mul, star_star, star_eq_conjTranspose (diagonal _), diagonal_conjTranspose,
mul_assoc]
congr!
ext
simp
