HaarPolynomial.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Normalization of the polynomial in a Haar unitary

Only the individual integer moments of the unitary enter these proofs. Freeness from another algebra is unnecessary here.

def OAI.KadisonKastler.unitaryHaarSum line 23
Source documentation
The first N positive powers of a unitary.
```
def unitaryHaarSum (N : ℕ) (v : unitary B) : B :=
…
```
def OAI.KadisonKastler.unitaryHaarPolynomial line 27
Source documentation
The scalar-recovery polynomial, normalized by the square root of N.
```
def unitaryHaarPolynomial (N : ℕ) (v : unitary B) : B :=
…
```
theorem OAI.KadisonKastler.unitaryHaarPolynomial_eq_real_smul line 30

theorem OAI.KadisonKastler.trace_haarPower_pair line 35

Source documentation

Distinct integer powers are orthogonal for the Haar trace.

theorem trace_haarPower_pair (τ : FaithfulTracialState B) (v : unitary B)
    (hhaar : ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower v k) = 0)
    (k l : ℤ) :
    τ.toLinearMap (star (haarPower v k) * haarPower v l) =
      if k = l then 1 else 0 := by
…

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

theorem OAI.KadisonKastler.trace_unitaryHaarSum_square line 48
theorem OAI.KadisonKastler.trace_unitaryHaarPolynomial line 62

theorem OAI.KadisonKastler.trace_unitaryHaarPolynomial_square line 73

Source documentation

Unit Haar second moment of the normalized polynomial.

theorem trace_unitaryHaarPolynomial_square (τ : FaithfulTracialState B) (v : unitary B)
    (hhaar : ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower v k) = 0)
    {N : ℕ} (hN : 0 < N) :
    τ.toLinearMap (star (unitaryHaarPolynomial N v) * unitaryHaarPolynomial N v) = 1 := by
…

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

theorem OAI.KadisonKastler.norm_unitaryHaarSum_le line 90
Source documentation
The triangle inequality gives the uniform polynomial norm bound.
```
theorem norm_unitaryHaarSum_le (N : ℕ) (v : unitary B) :
    ‖unitaryHaarSum N v‖ ≤ (N : ℝ) := by
…
```
Mentions: OAI.KadisonKastler.unitaryHaarSum
theorem OAI.KadisonKastler.norm_unitaryHaarPolynomial_le_sqrt line 105
theorem OAI.KadisonKastler.norm_unitaryHaarPolynomial_mul_self_le line 118
theorem OAI.KadisonKastler.FreeHaarMoments.trace_unitaryHaarPolynomial_square line 127
theorem OAI.KadisonKastler.map_unitaryHaarPolynomial_character line 135
Source documentation
Evaluation at a circle character recovers the scalar polynomial used in the angular Haar-tail calculation.
```
theorem map_unitaryHaarPolynomial_character (φ : B →⋆ₐ[ℂ] ℂ) (N : ℕ)
    (v : unitary B) (t : ℝ) (hv : φ (v : B) = Complex.exp (Complex.I * (t : ℂ))) :
    φ (unitaryHaarPolynomial N v) = haarPolynomial N t := by
…
```
Mentions: OAI.KadisonKastler.unitaryHaarPolynomial, OAI.KadisonKastler.haarPolynomial