HaarRealSequence.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Real orthonormal tracial sequences from a Haar unitary

The normalized cosine combinations of the positive and negative powers of a Haar unitary are selfadjoint, trace zero, and orthonormal. Haar existence is not assumed to have been proved by this construction.

def OAI.KadisonSimilarity.haarCosineCoefficient line 19
Source documentation
This real scalar equals 1 / sqrt 2. The equivalent form is convenient for proving normalization without dividing by a square root.
```
def haarCosineCoefficient : ℂ := ((Real.sqrt 2 / 2 : ℝ) : ℂ)
```
theorem OAI.KadisonSimilarity.star_haarCosineCoefficient line 21
theorem OAI.KadisonSimilarity.haarCosineCoefficient_normalization line 25
def OAI.KadisonSimilarity.haarCosineVector line 36
Source documentation
The (n+1)-st normalized cosine of the algebraic Haar unitary.
```
def haarCosineVector (w : Rˣ) (n : ℕ) : R :=
…
```
theorem OAI.KadisonSimilarity.haarCosineVector_selfadjoint line 40
theorem OAI.KadisonSimilarity.haar_power_product_moment line 53
Source documentation
Multiplying integer powers turns the moment condition into a Kronecker delta for the sum of their exponents.
```
theorem haar_power_product_moment (j k : ℤ) :
    τ ((↑(w ^ j) : R) * (↑(w ^ k) : R)) = if j + k = 0 then 1 else 0 := by
…
```
theorem OAI.KadisonSimilarity.haarCosineVector_trace_zero line 59
theorem OAI.KadisonSimilarity.haarCosineVector_inner line 68
Source documentation
Distinct positive cosine frequencies are orthogonal. The two mixed terms survive exactly when the frequencies coincide.
```
theorem haarCosineVector_inner (hw : star w = w⁻¹) (i j : ℕ) :
    τ (star (haarCosineVector w i) * haarCosineVector w j) =
      if i = j then 1 else 0 := by
…
```
Mentions: OAI.KadisonSimilarity.haarCosineVector
def OAI.KadisonSimilarity.realTracialSequenceOfHaar line 89
Source documentation
The algebraic real orthonormal sequence required by the tracial matrix tower is constructed from the Haar unitary.
```
def realTracialSequenceOfHaar (hw : star w = w⁻¹) : RealTracialSequence τ where
…
```
Mentions: OAI.KadisonSimilarity.RealTracialSequence

def OAI.KadisonSimilarity.tracialMatrixTowerOfHaar line 101

Source documentation

A Haar unitary removes the independent real-orthonormal-sequence input from the tracial matrix tower construction.

def tracialMatrixTowerOfHaar
    (V : R →ₗ[ℂ] E) (L : R →⋆ₐ[ℂ] (E →L[ℂ] E))
    (hinner : ∀ a b, inner ℂ (V a) (V b) = τ (star a * b))
    (hleft : ∀ a b, L a (V b) = V (a * b))
    (htrace : ∀ a b, τ (a * b) = τ (b * a))
    (M : NestedTracialMatrices (A := A) τ V) (hw : star w = w⁻¹)
…

Mentions: OAI.KadisonSimilarity.NestedTracialMatrices