HaarFunctionalCalculus.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The continuous Haar trace formula

An explicit continuous functional calculus is determined here by its values on Fourier monomials. Fourier density and the integer Haar moments identify its trace with normalized angular Haar integration.

abbrev OAI.KadisonKastler.HaarCircle line 22
def OAI.KadisonKastler.haarCircleIntegral line 27
Source documentation
Integration of continuous functions against probability Haar measure.
```
def haarCircleIntegral : C(HaarCircle, ℂ) →L[ℂ] ℂ :=
…
```
Mentions: OAI.KadisonKastler.HaarCircle
theorem OAI.KadisonKastler.haarCircleIntegral_apply line 32
theorem OAI.KadisonKastler.haarCircleIntegral_fourier line 40
def OAI.KadisonKastler.traceCLM line 51

theorem OAI.KadisonKastler.haar_functional_trace line 57

Source documentation

Matching the Fourier monomials with Haar powers determines the trace of every continuous function.

theorem haar_functional_trace (τ : FaithfulTracialState B) (v : unitary B)
    (hhaar : ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower v k) = 0)
    (Φ : C(HaarCircle, ℂ) →⋆ₐ[ℂ] B)
    (hΦ : ∀ n : ℤ, Φ (fourier n) = haarPower v n) (g : C(HaarCircle, ℂ)) :
    τ.toLinearMap (Φ g) = ∫ t, g t ∂(AddCircle.haarAddCircle (T := 2 * Real.pi)) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.HaarCircle

theorem OAI.KadisonKastler.FreeHaarMoments.functional_trace line 81

theorem OAI.KadisonKastler.haar_functional_trace_square line 89

Source documentation

The continuous calculus preserves the scalar Haar square integral.

theorem haar_functional_trace_square (τ : FaithfulTracialState B) (v : unitary B)
    (hhaar : ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower v k) = 0)
    (Φ : C(HaarCircle, ℂ) →⋆ₐ[ℂ] B)
    (hΦ : ∀ n : ℤ, Φ (fourier n) = haarPower v n) (g : C(HaarCircle, ℂ)) :
    τ.toLinearMap (star (Φ g) * Φ g) =
      ((∫ t, ‖g t‖ ^ 2 ∂(AddCircle.haarAddCircle (T := 2 * Real.pi))) : ℝ) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.HaarCircle

theorem OAI.KadisonKastler.traceTwoNorm_haar_functional line 106

Source documentation

In particular, its tracial two-norm is the scalar Haar L² norm.

theorem traceTwoNorm_haar_functional (τ : FaithfulTracialState B) (v : unitary B)
    (hhaar : ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower v k) = 0)
    (Φ : C(HaarCircle, ℂ) →⋆ₐ[ℂ] B)
    (hΦ : ∀ n : ℤ, Φ (fourier n) = haarPower v n) (g : C(HaarCircle, ℂ)) :
    traceTwoNorm τ (Φ g) =
      Real.sqrt (∫ t, ‖g t‖ ^ 2 ∂(AddCircle.haarAddCircle (T := 2 * Real.pi))) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.HaarCircle, OAI.KadisonKastler.traceTwoNorm

theorem OAI.KadisonKastler.map_fourierSpan_mem_haarLaurentSpan line 115
theorem OAI.KadisonKastler.exists_haarLaurent_approx_of_functional line 133
Source documentation
Fourier density supplies actual Laurent approximants to every continuous function of the Haar unitary.
```
theorem exists_haarLaurent_approx_of_functional (τ : FaithfulTracialState B)
    (v : unitary B) (Φ : C(HaarCircle, ℂ) →⋆ₐ[ℂ] B)
    (hΦ : ∀ n : ℤ, Φ (fourier n) = haarPower v n) (g : C(HaarCircle, ℂ)) :
    ∃ c : ℕ → B, (∀ n, c n ∈ haarLaurentSpan v) ∧
      Tendsto (fun n => traceTwoNorm τ (c n - Φ g)) atTop (𝓝 0) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.HaarCircle, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.haarLaurentSpan, OAI.KadisonKastler.traceTwoNorm