FreeDihedral.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The Haar and reflection-coset moments of two free centered symmetries, derived directly from alternating-centered-word freeness.

def OAI.KadisonSimilarity.pairedWord line 15
theorem OAI.KadisonSimilarity.pairedWord_prod line 20
theorem OAI.KadisonSimilarity.pairedWord_alternating line 26
theorem OAI.KadisonSimilarity.ScalarFree.symm line 35
Source documentation
Exchanging the free factors exchanges the alternating starting side.
```
theorem ScalarFree.symm {τ : R →ₗ[ℂ] ℂ} {P Q : StarSubalgebra ℂ R}
    (h : ScalarFree τ P Q) : ScalarFree τ Q P := by
…
```
Mentions: OAI.KadisonSimilarity.ScalarFree

theorem OAI.KadisonSimilarity.ScalarFree.trace_pair_power line 50

Source documentation

Every positive power of the product of free centered letters has trace zero.

theorem ScalarFree.trace_pair_power {τ : R →ₗ[ℂ] ℂ} {P Q : StarSubalgebra ℂ R}
    (hf : ScalarFree τ P Q) {d s : R}
    (hd : d ∈ P) (hs : s ∈ Q) (hd0 : τ d = 0) (hs0 : τ s = 0)
    {n : ℕ} (hn : 0 < n) : τ ((d * s) ^ n) = 0 := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree

theorem OAI.KadisonSimilarity.pairedWord_append_alternating line 60

theorem OAI.KadisonSimilarity.ScalarFree.trace_pair_power_mul_first line 69

Source documentation

The odd alternating words, which form the reflection coset, also vanish.

theorem ScalarFree.trace_pair_power_mul_first
    {τ : R →ₗ[ℂ] ℂ} {P Q : StarSubalgebra ℂ R} (hf : ScalarFree τ P Q)
    {d s : R} (hd : d ∈ P) (hs : s ∈ Q) (hd0 : τ d = 0) (hs0 : τ s = 0)
    (n : ℕ) : τ ((d * s) ^ n * d) = 0 := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree

theorem OAI.KadisonSimilarity.free_symmetry_haar_moments line 83

Source documentation

Two free centered symmetries have a product whose nonzero integer moments vanish.

theorem free_symmetry_haar_moments
    (τ : R →ₗ[ℂ] ℂ) (hτ : τ 1 = 1)
    (P Q : StarSubalgebra ℂ R) (hf : ScalarFree τ P Q)
    (d s : Rˣ) (hd : (d : R) ∈ P) (hs : (s : R) ∈ Q)
    (hd0 : τ (d : R) = 0) (hs0 : τ (s : R) = 0)
    (hdinv : d⁻¹ = d) (hsinv : s⁻¹ = s) (l : ℤ) :
    τ (↑((d * s) ^ l) : R) = if l = 0 then 1 else 0 := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree

theorem OAI.KadisonSimilarity.free_symmetry_coset_moments line 106

Source documentation

Every reflection-coset word has zero trace.

theorem free_symmetry_coset_moments
    (τ : R →ₗ[ℂ] ℂ) (P Q : StarSubalgebra ℂ R) (hf : ScalarFree τ P Q)
    (d s : Rˣ) (hd : (d : R) ∈ P) (hs : (s : R) ∈ Q)
    (hd0 : τ (d : R) = 0) (hs0 : τ (s : R) = 0)
    (hdinv : d⁻¹ = d) (hsinv : s⁻¹ = s) (l : ℤ) :
    τ ((↑((d * s) ^ l) : R) * (s : R)) = 0 := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree

theorem OAI.KadisonSimilarity.free_symmetry_product_star line 132

Source documentation

The product of two selfadjoint involutions is unitary.

theorem free_symmetry_product_star (d s : Rˣ)
    (hd : star d = d) (hs : star s = s) (hdi : d⁻¹ = d) (hsi : s⁻¹ = s) :
    star (d * s) = (d * s)⁻¹ := by
…

theorem OAI.KadisonSimilarity.tracial_haar_powers_orthonormal line 140

Source documentation

Haar moments give orthonormal nonnegative powers in the tracial Hilbert space. This is the weak-null family used in the corner argument.

theorem tracial_haar_powers_orthonormal
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    (τ : R →ₗ[ℂ] ℂ) (V : R →ₗ[ℂ] H)
    (hinner : ∀ a b, inner ℂ (V a) (V b) = τ (star a * b))
    (w : Rˣ) (hw : star w = w⁻¹)
    (hhaar : ∀ l : ℤ, τ (↑(w ^ l) : R) = if l = 0 then 1 else 0) :
    Orthonormal ℂ (fun n : ℕ => V (↑(w ^ (n : ℤ)) : R)) := by
…