Theorems · Definition · functional analysis

Matrix.IsHermitian.cfc

{n : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : RCLike 𝕜] → [Fintype n] → [DecidableEq n] → {A : Matrix n n 𝕜} → A.IsHermitian → (ℝ → ℝ) → Matrix n n 𝕜

The continuous functional calculus of a Hermitian matrix as a triple product using the spectral theorem. Note that this actually operates on bare functions since every function is continuous on the spectrum of a matrix, since the spectrum is finite. This is shown to be equal to the generic continuous functional calculus API in Matrix.IsHermitian.cfc_eq. In general, users should prefer the generic API, especially because it will make rewriting easier.

Defined in

Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Cited by

2 results in Mathlib

Foundations

Depth 258 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeFintypeDecidableEq