UnitaryFunctionalCalculus.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The circle functional calculus of an actual unitary

The homomorphism needed by the Haar trace formula is constructed from ordinary continuous functional calculus on the unitary's spectrum.

def OAI.KadisonKastler.unitarySpectrumCircle line 20
Source documentation
The unitary spectrum as a continuous map into the circle.
```
def unitarySpectrumCircle (u : unitary B) : C(spectrum ℂ (u : B), Circle) where
…
```
def OAI.KadisonKastler.unitarySpectrumAngle line 25
Source documentation
Angular coordinates on the spectrum, taken in the quotient circle.
```
def unitarySpectrumAngle (u : unitary B) : C(spectrum ℂ (u : B), HaarCircle) :=
…
```
Mentions: OAI.KadisonKastler.HaarCircle
def OAI.KadisonKastler.unitaryCircleCFC line 29
Source documentation
Actual circle functional calculus in the supplied C*-algebra.
```
def unitaryCircleCFC (u : unitary B) : C(HaarCircle, ℂ) →⋆ₐ[ℂ] B :=
…
```
Mentions: OAI.KadisonKastler.HaarCircle
theorem OAI.KadisonKastler.toCircle_eq_homeomorph line 33
theorem OAI.KadisonKastler.fourier_one_spectrum line 40
theorem OAI.KadisonKastler.unitaryCircleCFC_fourier_one line 51
Source documentation
The degree-one circle function evaluates to the original unitary.
```
theorem unitaryCircleCFC_fourier_one (u : unitary B) :
    unitaryCircleCFC u (fourier 1) = (u : B) := by
…
```
Mentions: OAI.KadisonKastler.unitaryCircleCFC
theorem OAI.KadisonKastler.fourier_add_map line 57
theorem OAI.KadisonKastler.unitaryCircleCFC_fourier_nat line 63
theorem OAI.KadisonKastler.unitaryCircleCFC_fourier line 74
Source documentation
Every integer Fourier monomial evaluates to the corresponding actual unitary power, supplying the hypothesis of the continuous Haar formula.
```
theorem unitaryCircleCFC_fourier (u : unitary B) (n : ℤ) :
    unitaryCircleCFC u (fourier n) = haarPower u n := by
…
```
Mentions: OAI.KadisonKastler.unitaryCircleCFC, OAI.KadisonKastler.haarPower
theorem OAI.KadisonKastler.trace_unitaryCircleCFC line 93
Source documentation
Haar moments alone determine the trace of the constructed circle functional calculus, without an additional representation hypothesis.
```
theorem trace_unitaryCircleCFC (τ : FaithfulTracialState B) (u : unitary B)
    (hhaar : ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower u k) = 0)
    (g : C(HaarCircle, ℂ)) :
    τ.toLinearMap (unitaryCircleCFC u g) = haarCircleIntegral g := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.HaarCircle, OAI.KadisonKastler.unitaryCircleCFC, OAI.KadisonKastler.haarCircleIntegral