FreeHaar.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Free Haar moments imply freeness of the conjugated diagonals

The hypothesis records ordinary alternating centered moments with nonzero interior Haar powers. The last power may be zero. A telescoping product identity and traciality convert products from conjugated copies into exactly these moments. No free-diagonal conclusion is a field of the hypothesis.

def OAI.KadisonKastler.haarPower line 27
theorem OAI.KadisonKastler.haarPower_zero line 30
theorem OAI.KadisonKastler.haarPower_add line 33
theorem OAI.KadisonKastler.haarPower_neg line 37
theorem OAI.KadisonKastler.haarPower_natCast line 42
theorem OAI.KadisonKastler.haarPower_sub_mul line 46
structure OAI.KadisonKastler.FreeHaarMoments line 53
Source documentation
Standard alternating centered moments of a subalgebra free from a Haar unitary. Every interior exponent is nonzero; the final Haar letter is optional.
```
structure FreeHaarMoments (τ : FaithfulTracialState B) (A : StarSubalgebra ℂ B)
    (u : unitary B) : Prop where
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
def OAI.KadisonKastler.differenceLetters line 61
theorem OAI.KadisonKastler.differenceLetters_first line 67
theorem OAI.KadisonKastler.length_differenceLetters line 77
theorem OAI.KadisonKastler.differenceLetters_property line 83
theorem OAI.KadisonKastler.differenceLetters_nonzero line 94

theorem OAI.KadisonKastler.conjugateProduct_eq line 115

Source documentation

The product telescopes before any moment condition is used.

private theorem conjugateProduct_eq (u : unitary B) (last : ℤ) (x : B × ℤ)
    (l : List (B × ℤ)) :
    ((x :: l).map (fun y => haarPower u (-y.2) * y.1 * haarPower u y.2)).prod =
      haarPower u (-x.2) *
        ((differenceLetters last (x :: l)).map (fun y => y.1 * haarPower u y.2)).prod *
          haarPower u last := by
…

Mentions: OAI.KadisonKastler.haarPower, OAI.KadisonKastler.differenceLetters

theorem OAI.KadisonKastler.trace_haar_conjugate line 130
theorem OAI.KadisonKastler.FreeHaarMoments.alternating_list line 140

theorem OAI.KadisonKastler.FreeHaarMoments.trace_conjugateProduct_eq_zero line 157

Source documentation

Adjacent distinct conjugating powers turn into the nonzero interior Haar powers required by the alternating centered moment condition.

theorem trace_conjugateProduct_eq_zero (h : FreeHaarMoments τ A u)
    (l : List (B × ℤ)) (hl : l ≠ [])
    (hmem : ∀ x ∈ l, x.1 ∈ A) (hcentered : ∀ x ∈ l, τ.toLinearMap x.1 = 0)
    (hexp : l.IsChain (fun x y => x.2 ≠ y.2)) :
    τ.toLinearMap ((l.map (fun x => haarPower u (-x.2) * x.1 * haarPower u x.2)).prod) = 0 := by
…

Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.haarPower

theorem OAI.KadisonKastler.FreeHaarMoments.scalarFree_conjugatedDiagonal line 177
Source documentation
Equal-trace diagonal partitions conjugated by distinct powers of a free Haar unitary form a scalar-free family.
```
theorem scalarFree_conjugatedDiagonal (h : FreeHaarMoments τ A u)
    {r d : ℕ} (e : Fin d → B)
    (hmem : ∀ a, e a ∈ A) (htrace : ∀ a, τ.toLinearMap (e a) = (d : ℂ)⁻¹) :
    ScalarFreeDiagonal τ (conjugatedDiagonal e (u : B) r) := by
…
```
Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.ScalarFreeDiagonal, OAI.KadisonKastler.conjugatedDiagonal