English
For any Hermitian A and any real-valued function f, the two formulations of the functional calculus agree: the canonical cfc built from the spectral data equals the explicit cfc given by the real-to-matrix map.
Русский
Для любой эрмитовой A и любой функции f значения двух форм функционального калькулятора совпадают: канонический cfc, построенный по спектральным данным, равен явному cfc, заданному соответствием по действительным значениям.
LaTeX
$$cfc f A = hA.cfc f$$
Lean4
theorem cfc_eq (f : ℝ → ℝ) : cfc f A = hA.cfc f :=
by
have hA' : IsSelfAdjoint A := hA
have := cfcHom_eq_of_continuous_of_map_id hA' hA.cfcAux hA.isClosedEmbedding_cfcAux.continuous hA.cfcAux_id
rw [cfc_apply f A hA' (by rw [continuousOn_iff_continuous_restrict]; fun_prop), this]
simp only [cfcAux_apply, ContinuousMap.coe_mk, Function.comp_def, Set.restrict_apply, IsHermitian.cfc]
