FreeExpectation.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The expectation of a free compression

Scalar tracial freeness is expressed by vanishing alternating centered words. The formula E(e b e) = τ(e)^2 b is derived by testing against the second algebra, rather than included among the free-product input data.

inductive OAI.KadisonSimilarity.AlternatingCenteredWord line 20

Source documentation

An alternating word of centered letters in two specified algebras.

inductive AlternatingCenteredWord (τ : R →ₗ[ℂ] ℂ) (P Q : StarSubalgebra ℂ R) :
    Bool → List R → Prop
  | nil (side : Bool) : AlternatingCenteredWord τ P Q side []
  | cons {side : Bool} {x : R} {xs : List R}
      (hmem : x ∈ if side then P else Q) (hzero : τ x = 0)
      (htail : AlternatingCenteredWord τ P Q (!side) xs) :
      AlternatingCenteredWord τ P Q side (x :: xs)

/-- Scalar freeness, in the alternating-centered-word convention of the paper. -/

def OAI.KadisonSimilarity.ScalarFree line 29
Source documentation
Scalar freeness, in the alternating-centered-word convention of the paper.
```
def ScalarFree (τ : R →ₗ[ℂ] ℂ) (P Q : StarSubalgebra ℂ R) : Prop :=
…
```
theorem OAI.KadisonSimilarity.ScalarFree.trace_pair line 37
theorem OAI.KadisonSimilarity.ScalarFree.trace_triple line 43
theorem OAI.KadisonSimilarity.ScalarFree.trace_quadruple line 50
def OAI.KadisonSimilarity.traceCentered line 62
Source documentation
Centering uses the normalized trace.
```
def traceCentered (τ : R →ₗ[ℂ] ℂ) (a : R) : R := a - τ a • 1
```
theorem OAI.KadisonSimilarity.traceCentered_mem line 64
theorem OAI.KadisonSimilarity.traceCentered_trace line 69
theorem OAI.KadisonSimilarity.traceCentered_add line 73

theorem OAI.KadisonSimilarity.trace_centered_mul_of_free line 77

Source documentation

A centered letter is orthogonal, for the trace pairing, to the other algebra.

theorem trace_centered_mul_of_free
    (τ : R →ₗ[ℂ] ℂ) (hτ : τ 1 = 1) {P Q : StarSubalgebra ℂ R}
    (hf : ScalarFree τ P Q) {a b : R} (ha : a ∈ P) (ha0 : τ a = 0) (hb : b ∈ Q) :
    τ (a * b) = 0 := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree

theorem OAI.KadisonSimilarity.trace_test_free_compression_errors line 93

Source documentation

Orthogonality against the second algebra removes all three mixed terms in the free-compression expansion.

theorem trace_test_free_compression_errors
    (τ : R →ₗ[ℂ] ℂ) (hτ : τ 1 = 1)
    (htr : ∀ a b, τ (a * b) = τ (b * a))
    {P Q : StarSubalgebra ℂ R} (hf : ScalarFree τ P Q)
    {a b c : R} (ha : a ∈ P) (ha0 : τ a = 0)
    (hb : b ∈ Q) (hb0 : τ b = 0) (hc : c ∈ Q) :
    τ (c * (a * b)) = 0 ∧ τ (c * (b * a)) = 0 ∧ τ (c * (a * b * a)) = 0 := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree

theorem OAI.KadisonSimilarity.expectation_eq_of_trace_pairings line 135

Source documentation

The trace pairing determines the conditional expectation in a faithful tracial representation.

theorem expectation_eq_of_trace_pairings
    (τ : R →ₗ[ℂ] ℂ) (Q : StarSubalgebra ℂ R)
    (hfaithful : ∀ z, τ (star z * z) = 0 → z = 0)
    (E : R →ₗ[ℂ] R) (hE : ∀ x, E x ∈ Q)
    (htrace : ∀ x c, c ∈ Q → τ (c * E x) = τ (c * x))
    (x y : R) (hy : y ∈ Q)
    (hxy : ∀ c, c ∈ Q → τ (c * x) = τ (c * y)) : E x = y := by
…

theorem OAI.KadisonSimilarity.expectation_free_compression line 150

Source documentation

The expectation formula in lem:free-compression, proved from scalar freeness and the defining trace-pairing property of conditional expectation. The projection condition on e is not needed for this algebraic identity.

theorem expectation_free_compression
    (τ : R →ₗ[ℂ] ℂ) (hτ : τ 1 = 1)
    (htr : ∀ a b, τ (a * b) = τ (b * a))
    (hfaithful : ∀ z, τ (star z * z) = 0 → z = 0)
    {P Q : StarSubalgebra ℂ R} (hf : ScalarFree τ P Q)
    (E : R →ₗ[ℂ] R) (hE : ∀ x, E x ∈ Q)
    (htrace : ∀ x c, c ∈ Q → τ (c * E x) = τ (c * x))
    {e b : R} (he : e ∈ P) (hb : b ∈ Q) (hb0 : τ b = 0) :
    E (e * b * e) = (τ e) ^ 2 • b := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree