ConcreteRealSequence.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The dyadic signs in a diffuse finite tracial von Neumann algebra form the real tracial sequence required by the matrix-tower construction. The underlying projections have compatible dyadic refinements and orthogonality relations.

theorem OAI.KadisonSimilarity.concreteTraceLinear_eq_coordinateTraceLinear line 21
Source documentation
The two existing bundles contain the same vector trace.
```
theorem concreteTraceLinear_eq_coordinateTraceLinear (τ : TracialRepresentation M) :
    concreteTraceLinear τ = coordinateTraceLinear τ := by
…
```
Mentions: OAI.KadisonSimilarity.concreteTraceLinear
def OAI.KadisonSimilarity.concreteRademacher line 31
Source documentation
The successive dyadic signs, based at the identity projection.
```
def concreteRademacher (n : ℕ) : M.toStarSubalgebra :=
…
```
theorem OAI.KadisonSimilarity.concreteRademacher_star line 34
theorem OAI.KadisonSimilarity.concreteRademacher_square line 38
theorem OAI.KadisonSimilarity.concreteRademacher_trace line 42
theorem OAI.KadisonSimilarity.concreteRademacher_inner line 52
Source documentation
Refining earlier signs to the next finite dyadic algebra proves the off-diagonal moments; the diagonal follows from the square identity.
```
theorem concreteRademacher_inner (i j : ℕ) :
    concreteTraceLinear τ
      (star (concreteRademacher τ hdiff i) * concreteRademacher τ hdiff j) =
      if i = j then 1 else 0 := by
…
```
Mentions: OAI.KadisonSimilarity.concreteTraceLinear, OAI.KadisonSimilarity.concreteRademacher
def OAI.KadisonSimilarity.concreteRealTracialSequence line 65
Source documentation
A concrete diffuse tracial von Neumann algebra supplies the full real sequence without an independent orthonormal-sequence existence premise.
```
def concreteRealTracialSequence : RealTracialSequence (concreteTraceLinear τ) where
…
```
Mentions: OAI.KadisonSimilarity.RealTracialSequence, OAI.KadisonSimilarity.concreteTraceLinear