ConcreteHaarArc.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Construction of the spectral arc projection

Continuous circle cutoffs converge in the faithful tracial two-norm. Bounded completeness realizes their limit as a projection in the given von Neumann algebra, with its exact Haar mass and commutation relation.

structure OAI.KadisonKastler.HaarArcProjection line 27
Source documentation
The actual projection obtained from the continuous arc cutoffs.
```
structure HaarArcProjection (τ : FaithfulTracialState (Algebra M))
    (u : unitary (Algebra M)) (a : ℝ) where
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.nonempty_haarArcProjection line 39
Source documentation
The spectral arc projection is constructed, rather than assumed.
```
theorem nonempty_haarArcProjection (τ : FaithfulTracialState (Algebra M))
    (hτ : FiniteVectorTrace τ) (u : unitary (Algebra M))
    (hhaar : ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower u k) = 0) (a : ℝ) :
    Nonempty (HaarArcProjection τ u a) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.HaarArcProjection
theorem OAI.KadisonKastler.HaarArcProjection.commute line 59
Source documentation
The arc projection commutes with the unitary whose spectrum defines it.
```
theorem HaarArcProjection.commute {τ : FaithfulTracialState (Algebra M)}
    {u : unitary (Algebra M)} {a : ℝ} (E : HaarArcProjection τ u a) :
    Commute (u : Algebra M) E.projection := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.HaarArcProjection

theorem OAI.KadisonKastler.HaarArcProjection.trace line 86

Source documentation

The constructed projection has the normalized angular Haar mass.

theorem HaarArcProjection.trace {τ : FaithfulTracialState (Algebra M)}
    {u : unitary (Algebra M)} {a : ℝ} (E : HaarArcProjection τ u a)
    (hτ : FiniteVectorTrace τ)
    (hhaar : ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower u k) = 0)
    (ha : 0 ≤ a) (hapi : a ≤ Real.pi) :
    τ.toLinearMap E.projection = ((a / Real.pi : ℝ) : ℂ) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.HaarArcProjection, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.haarPower

theorem OAI.KadisonKastler.unitaryCircleCFC_haarCirclePolynomial line 104
Source documentation
The normalized scalar Fourier polynomial maps to the actual polynomial.
```
theorem unitaryCircleCFC_haarCirclePolynomial (u : unitary (Algebra M)) (N : ℕ) :
    unitaryCircleCFC u (haarCirclePolynomial N) = unitaryHaarPolynomial N u := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.unitaryCircleCFC, OAI.KadisonKastler.haarCirclePolynomial, OAI.KadisonKastler.unitaryHaarPolynomial
theorem OAI.KadisonKastler.HaarArcProjection.polynomial_commute line 113
Source documentation
Every polynomial in the unitary commutes with its arc projection.
```
theorem HaarArcProjection.polynomial_commute {τ : FaithfulTracialState (Algebra M)}
    {u : unitary (Algebra M)} {a : ℝ} (E : HaarArcProjection τ u a) (N : ℕ) :
    Commute (unitaryHaarPolynomial N u) E.projection := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.HaarArcProjection, OAI.KadisonKastler.unitaryHaarPolynomial

theorem OAI.KadisonKastler.HaarArcProjection.tail line 124

Source documentation

The constructed operator projection has exactly the scalar Haar tail energy for every normalized Fourier polynomial.

theorem HaarArcProjection.tail {τ : FaithfulTracialState (Algebra M)}
    {u : unitary (Algebra M)} {a : ℝ} (E : HaarArcProjection τ u a)
    (hτ : FiniteVectorTrace τ)
    (hhaar : ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower u k) = 0)
    (ha : 0 ≤ a) (hapi : a ≤ Real.pi) (N : ℕ) :
    (τ.toLinearMap (star (unitaryHaarPolynomial N u) * unitaryHaarPolynomial N u *
      (1 - E.projection))).re = haarTailEnergy N a := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.HaarArcProjection, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.unitaryHaarPolynomial, OAI.KadisonKastler.haarTailEnergy