SymmetryWordRange.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The base expectation on the algebra generated by the other free factor and one centered symmetry. The only density datum is the ordinary reduced word span; the two-dimensional expectation range is proved.

inductive OAI.KadisonSimilarity.CenteredSymmetryWord line 18

Source documentation

Alternating words in centered other-factor letters and one fixed symmetry. true means that the next letter comes from the other factor.

inductive CenteredSymmetryWord (τ : P →ₗ[ℂ] ℂ) (D : StarSubalgebra ℂ P) (s : P) :
    Bool → List P → Prop
  | nil (side : Bool) : CenteredSymmetryWord τ D s side []
  | other {d : P} {xs : List P} (hd : d ∈ D) (hzero : τ d = 0)
      (tail : CenteredSymmetryWord τ D s false xs) :
      CenteredSymmetryWord τ D s true (d :: xs)
  | symmetry {xs : List P} (tail : CenteredSymmetryWord τ D s true xs) :
      CenteredSymmetryWord τ D s false (s :: xs)

namespace CenteredSymmetryWord

variable {τ : P →ₗ[ℂ] ℂ} {D A : StarSubalgebra ℂ P} {s : P}

theorem OAI.KadisonSimilarity.CenteredSymmetryWord.alternating line 31
theorem OAI.KadisonSimilarity.CenteredSymmetryWord.expectation_span line 41
Source documentation
The expectation of a reduced word is either zero, the unit, or the specified symmetry. This follows from freeness and bimodularity.
```
theorem expectation_span
    (E : TracialExpectation τ A)
    (hfaithful : ∀ x, τ (star x * x) = 0 → x = 0)
    (hτ : τ 1 = 1) (hfree : ScalarFree τ D A)
    (hs : s ∈ A) (hs0 : τ s = 0)
    {side : Bool} {xs : List P} (h : CenteredSymmetryWord τ D s side xs) :
    ∃ α β : ℂ, E.map xs.prod = α • (1 : P) + β • s := by
…
```
Mentions: OAI.KadisonSimilarity.TracialExpectation, OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.CenteredSymmetryWord
def OAI.KadisonSimilarity.centeredSymmetryWordProducts line 75
Source documentation
Ordinary products of the alternating reduced symmetry words.
```
def centeredSymmetryWordProducts (τ : P →ₗ[ℂ] ℂ) (D : StarSubalgebra ℂ P) (s : P) :
    Set P := {x | ∃ (side : Bool) (xs : List P), CenteredSymmetryWord τ D s side xs ∧
…
```
Mentions: OAI.KadisonSimilarity.CenteredSymmetryWord

theorem OAI.KadisonSimilarity.TracialCornerGeometry.expectation_span_of_symmetry_word_density line 87

Source documentation

Passage from the actual reduced words to their L² closure supplies the word-algebra range hypothesis of the Fourier compression.

theorem expectation_span_of_symmetry_word_density
    (E : TracialExpectation G.trace A) (hfaithful : Function.Injective G.vector)
    (hτ : G.trace 1 = 1) (hfree : ScalarFree G.trace D A)
    (s : P) (hs : s ∈ A) (hs0 : G.trace s = 0)
    (hdense : ∀ x, x ∈ S → G.vector x ∈
      (Submodule.span ℂ (G.vector '' centeredSymmetryWordProducts G.trace D s)).topologicalClosure)
    (x : P) (hx : x ∈ S) :
    ∃ α β : ℂ, E.map x = α • (1 : P) + β • s := by
…

Mentions: OAI.KadisonSimilarity.TracialExpectation, OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.centeredSymmetryWordProducts