ReducedExpectation.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Reduced Haar words are orthogonal to the base algebra

These finite word calculations are the algebraic part of the conditional expectation argument. No conditional expectation existence or free-product norm theorem is assumed.

def OAI.KadisonKastler.centeredHaarWord line 21
Source documentation
An alternating word, with a base coefficient followed by each Haar power.
```
def centeredHaarWord (v : unitary B) (l : List (B × ℤ)) : B :=
…
```
theorem OAI.KadisonKastler.centeredHaarWord_nil line 25
theorem OAI.KadisonKastler.centeredHaarWord_cons line 28
def OAI.KadisonKastler.reducedHaarWord line 32
Source documentation
A reduced word with an initial Haar power.
```
def reducedHaarWord (v : unitary B) (q : ℤ) (l : List (B × ℤ)) : B :=
…
```
def OAI.KadisonKastler.appendLastExponent line 35
theorem OAI.KadisonKastler.appendLastExponent_fst line 41
theorem OAI.KadisonKastler.appendLastExponent_property line 51
theorem OAI.KadisonKastler.appendLastExponent_chain line 61
theorem OAI.KadisonKastler.centeredHaarWord_appendLastExponent line 78

theorem OAI.KadisonKastler.FreeHaarMoments.trace_centeredHaarWord_zero line 96

Source documentation

The finite-list form of the assumed ordinary centered Haar moments.

theorem trace_centeredHaarWord_zero (h : FreeHaarMoments τ A v)
    (l : List (B × ℤ)) (hl : l ≠ [])
    (hmem : ∀ x ∈ l, x.1 ∈ A) (hz : ∀ x ∈ l, τ.toLinearMap x.1 = 0)
    (hk : l.IsChain (fun x _ => x.2 ≠ 0)) :
    τ.toLinearMap (centeredHaarWord v l) = 0 := by
…

Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.centeredHaarWord

theorem OAI.KadisonKastler.FreeHaarMoments.trace_reducedHaarWord_zero line 111

Source documentation

An initial Haar letter can be moved to the final exponent by traciality.

theorem trace_reducedHaarWord_zero (h : FreeHaarMoments τ A v)
    (q : ℤ) (hq : q ≠ 0) (l : List (B × ℤ))
    (hmem : ∀ x ∈ l, x.1 ∈ A) (hz : ∀ x ∈ l, τ.toLinearMap x.1 = 0)
    (hk : l.IsChain (fun x _ => x.2 ≠ 0)) :
    τ.toLinearMap (reducedHaarWord v q l) = 0 := by
…

Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.reducedHaarWord

theorem OAI.KadisonKastler.FreeHaarMoments.trace_base_mul_reducedHaarWord_zero line 131

Source documentation

Every reduced word with a nonzero leading Haar exponent is trace orthogonal to the whole base algebra.

theorem trace_base_mul_reducedHaarWord_zero (h : FreeHaarMoments τ A v)
    (q : ℤ) (hq : q ≠ 0) (l : List (B × ℤ))
    (hmem : ∀ x ∈ l, x.1 ∈ A) (hz : ∀ x ∈ l, τ.toLinearMap x.1 = 0)
    (hk : l.IsChain (fun x _ => x.2 ≠ 0)) {b : B} (hb : b ∈ A) :
    τ.toLinearMap (b * reducedHaarWord v q l) = 0 := by
…

Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.reducedHaarWord

theorem OAI.KadisonKastler.FreeHaarMoments.trace_base_mul_sandwiched_reducedHaarWord_zero line 162

Source documentation

Exterior base-algebra factors preserve the reduced-word orthogonality.

theorem trace_base_mul_sandwiched_reducedHaarWord_zero (h : FreeHaarMoments τ A v)
    (q : ℤ) (hq : q ≠ 0) (l : List (B × ℤ))
    (hmem : ∀ x ∈ l, x.1 ∈ A) (hz : ∀ x ∈ l, τ.toLinearMap x.1 = 0)
    (hk : l.IsChain (fun x _ => x.2 ≠ 0)) {b x y : B}
    (hb : b ∈ A) (hx : x ∈ A) (hy : y ∈ A) :
    τ.toLinearMap (b * (x * reducedHaarWord v q l * y)) = 0 := by
…

Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.reducedHaarWord

theorem OAI.KadisonKastler.eq_zero_of_mem_base_of_trace_pairings line 180
Source documentation
Faithfulness identifies a base element from all of its trace pairings.
```
theorem eq_zero_of_mem_base_of_trace_pairings (τ : FaithfulTracialState B)
    (A : StarSubalgebra ℂ B) {x : B} (hx : x ∈ A)
    (hpair : ∀ b ∈ A, τ.toLinearMap (b * x) = 0) : x = 0 := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState

theorem OAI.KadisonKastler.FreeHaarMoments.reducedHaarWord_expectation_zero line 187

Source documentation

Any trace-preserving base projection therefore kills the reduced word. Only its defining range and trace-pairing properties are required here.

theorem FreeHaarMoments.reducedHaarWord_expectation_zero
    {τ : FaithfulTracialState B} {A : StarSubalgebra ℂ B} {v : unitary B}
    (h : FreeHaarMoments τ A v) (E : B →ₗ[ℂ] B)
    (hE : ∀ x, E x ∈ A)
    (hpair : ∀ b ∈ A, ∀ x, τ.toLinearMap (b * E x) = τ.toLinearMap (b * x))
    (q : ℤ) (hq : q ≠ 0) (l : List (B × ℤ))
    (hmem : ∀ x ∈ l, x.1 ∈ A) (hz : ∀ x ∈ l, τ.toLinearMap x.1 = 0)
    (hk : l.IsChain (fun x _ => x.2 ≠ 0)) :
    E (reducedHaarWord v q l) = 0 := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.reducedHaarWord