English
There exists a continuous functional calculus for a Hermitian matrix A over a real-field realization; equivalently, a canonical homomorphism assigns to each real-valued continuous function on the spectrum of A a matrix in the ambient algebra, preserving addition, multiplication and star, and extending the spectral calculus.
Русский
Существует непрерывный функциональный калькулятор для эрмитовой матрицы A над реализацией вещественного поля: к каждой вещественно-значной непрерывной функции на спектре A ставится соответствующая матрица, сохраняющая сложение, умножение и сопряжение, продолжая спектральный калькулятор.
LaTeX
$$∃ cfc : C(spectrum ℝ A, ℝ) →⋆ₐ[ℝ] M_n(𝕜) (star-algebra homomorphism) for IsSelfAdjoint A$$
Lean4
/-- Instance of the continuous functional calculus for a Hermitian matrix over `𝕜` with
`RCLike 𝕜`. -/
instance instContinuousFunctionalCalculus : ContinuousFunctionalCalculus ℝ (Matrix n n 𝕜) IsSelfAdjoint
where
exists_cfc_of_predicate a
ha := by
replace ha : IsHermitian a := ha
refine ⟨ha.cfcAux, ha.isClosedEmbedding_cfcAux, ha.cfcAux_id, fun f ↦ ?map_spec, fun f ↦ ?hermitian⟩
case map_spec =>
apply Set.eq_of_subset_of_subset
· rw [← ContinuousMap.spectrum_eq_range f]
apply AlgHom.spectrum_apply_subset
· rw [cfcAux_apply, unitary.spectrum.unitary_conjugate]
rintro - ⟨x, rfl⟩
apply spectrum.of_algebraMap_mem 𝕜
simp only [Function.comp_apply, Set.mem_range, spectrum_diagonal]
obtain ⟨x, hx⟩ := x
obtain ⟨i, rfl⟩ := ha.spectrum_real_eq_range_eigenvalues ▸ hx
exact ⟨i, rfl⟩
case hermitian =>
simp only [isSelfAdjoint_iff, cfcAux_apply, mul_assoc, star_mul, star_star]
rw [star_eq_conjTranspose, diagonal_conjTranspose]
congr!
simp [Pi.star_def, Function.comp_def]
spectrum_nonempty a
ha := by
obtain (h | h) := isEmpty_or_nonempty n
· obtain ⟨x, y, hxy⟩ := exists_pair_ne (Matrix n n 𝕜)
exact False.elim <| Matrix.of.symm.injective.ne hxy <| Subsingleton.elim _ _
· exact spectrum_real_eq_range_eigenvalues ha ▸ Set.range_nonempty _
predicate_zero := .zero _
