SymmetryExpectation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Identifying a tracial expectation whose range lies in the two-dimensional algebra generated by a centered symmetry. The Fourier identities then require only scalar trace moments, not operator-valued moment assumptions.

theorem OAI.KadisonSimilarity.TracialExpectation.map_eq_symmetryExpectation line 20
Source documentation
Trace preservation and the trace pairing with s determine both coefficients of the conditional expectation.
```
theorem map_eq_symmetryExpectation (E : TracialExpectation τ A)
    (hτ : τ 1 = 1) (s : P) (hsA : s ∈ A) (hs0 : τ s = 0) (hs2 : s * s = 1)
    (x : P) (hspan : ∃ α β : ℂ, E.map x = α • (1 : P) + β • s) :
    E.map x = symmetryExpectation τ s x := by
…
```
Mentions: OAI.KadisonSimilarity.TracialExpectation, OAI.KadisonSimilarity.symmetryExpectation

theorem OAI.KadisonSimilarity.TracialExpectation.rotation_reflection_of_scalar_moments line 37

Source documentation

The rotation and reflection expectation identities follow from scalar Fourier moments once the free-word calculation puts these expectations in span{1,s}.

theorem rotation_reflection_of_scalar_moments (E : TracialExpectation τ A)
    (hτ : τ 1 = 1) (htr : ∀ x y, τ (x * y) = τ (y * x))
    (s : P) (hsA : s ∈ A) (hs0 : τ s = 0) (hs2 : s * s = 1)
    (x : P) (γ : ℂ) (hcoef : τ x = γ) (hcoset : τ (s * x) = 0)
    (hspan : ∃ α β : ℂ, E.map x = α • (1 : P) + β • s)
    (hspan' : ∃ α β : ℂ, E.map (x * s) = α • (1 : P) + β • s) :
    E.map x = γ • (1 : P) ∧ E.map (x * s) = γ • s := by
…

Mentions: OAI.KadisonSimilarity.TracialExpectation

theorem OAI.KadisonSimilarity.TracialExpectation.restricted_tower_of_symmetry_span line 51

Source documentation

On the word algebra, a two-dimensional base expectation factors through any intermediate algebra containing the symmetry. No global tower inclusion of the entire base algebra is required.

theorem restricted_tower_of_symmetry_span (E : TracialExpectation τ A)
    {C S : StarSubalgebra ℂ P} (EC : TracialExpectation τ C) (hCS : C ≤ S)
    (hτ : τ 1 = 1) (s : P) (hsA : s ∈ A) (hsC : s ∈ C)
    (hs0 : τ s = 0) (hs2 : s * s = 1)
    (hspan : ∀ x, x ∈ S → ∃ α β : ℂ, E.map x = α • (1 : P) + β • s)
    (x : P) (hx : x ∈ S) : E.map (EC.map x) = E.map x := by
…

Mentions: OAI.KadisonSimilarity.TracialExpectation

theorem OAI.KadisonSimilarity.TracialExpectation.dihedral_entry_of_scalar_moments line 64

Source documentation

The dihedral Fourier entry with actual trace-pairing expectations. Only scalar Fourier moments and the base word-range calculation remain; bimodularity and the correctly restricted tower identity are derived.

theorem dihedral_entry_of_scalar_moments (E : TracialExpectation τ A)
    {C S : StarSubalgebra ℂ P} (EC : TracialExpectation τ C) (hCS : C ≤ S)
    (hfaithful : ∀ x, τ (star x * x) = 0 → x = 0)
    (hτ : τ 1 = 1) (htr : ∀ x y, τ (x * y) = τ (y * x))
    (w d : Pˣ) (hd : d * w = w⁻¹ * d)
    (hsA : (↑(w⁻¹ * d) : P) ∈ A) (hsC : (↑(w⁻¹ * d) : P) ∈ C)
    (hs0 : τ (↑(w⁻¹ * d) : P) = 0)
    (hs2 : (↑(w⁻¹ * d) : P) * (↑(w⁻¹ * d) : P) = 1)
    (hspan : ∀ x, x ∈ S → ∃ α β : ℂ,
      E.map x = α • (1 : P) + β • (↑(w⁻¹ * d) : P))
    (hpower : ∀ j : ℤ, (↑(w ^ j) : P) ∈ C)
    (f h : P) (hf : f ∈ C) (hh : h ∈ S) (u : ℂ) (γ : ℤ → ℂ)
…

Mentions: OAI.KadisonSimilarity.TracialExpectation