TracialExpectations.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The trace-pairing description of conditional expectation. Its uniqueness, bimodule law, tower law, and Hilbert projection formula are derived here.

structure OAI.KadisonSimilarity.TracialExpectation line 18
Source documentation
The minimal trace-pairing data for expectation onto a tracial subalgebra. Existence is required only when a subalgebra is realized as a von Neumann subalgebra; no existence assertion for arbitrary star subalgebras is made.
```
structure TracialExpectation (τ : P →ₗ[ℂ] ℂ) (A : StarSubalgebra ℂ P) where
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.trace_faithful line 27
Source documentation
Faithfulness of the algebra-vector realization implies faithfulness of its positive trace pairing.
```
theorem trace_faithful (G : TracialCornerGeometry P H)
    (hfaithful : Function.Injective G.vector) (x : P)
    (hx : G.trace (star x * x) = 0) : x = 0 := by
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry
theorem OAI.KadisonSimilarity.TracialExpectation.trace_map line 42
Source documentation
Expectation preserves the trace by testing its pairing with the unit.
```
theorem trace_map (x : P) : τ (E.map x) = τ x := by
…
```
theorem OAI.KadisonSimilarity.TracialExpectation.eq_of_pairings line 50
Source documentation
The trace pairing determines each expectation value uniquely.
```
theorem eq_of_pairings (x y : P) (hy : y ∈ A)
    (hxy : ∀ c, c ∈ A → τ (c * x) = τ (c * y)) : E.map x = y :=
…
```
theorem OAI.KadisonSimilarity.TracialExpectation.map_of_mem line 54
theorem OAI.KadisonSimilarity.TracialExpectation.map_one line 57
theorem OAI.KadisonSimilarity.TracialExpectation.map_map line 59
theorem OAI.KadisonSimilarity.TracialExpectation.map_mul_left line 63
Source documentation
Left bimodularity follows from the trace-pairing characterization alone.
```
theorem map_mul_left (a x : P) (ha : a ∈ A) : E.map (a * x) = a * E.map x := by
…
```
theorem OAI.KadisonSimilarity.TracialExpectation.map_mul_right line 69
Source documentation
Right bimodularity additionally uses traciality.
```
theorem map_mul_right (htr : ∀ x y, τ (x * y) = τ (y * x))
    (x b : P) (hb : b ∈ A) : E.map (x * b) = E.map x * b := by
…
```
theorem OAI.KadisonSimilarity.TracialExpectation.bimodule line 78
theorem OAI.KadisonSimilarity.TracialExpectation.tower line 84
Source documentation
Nested tracial expectations compose to the smaller one.
```
theorem tower {C : StarSubalgebra ℂ P} (EC : TracialExpectation τ C)
    (hAC : A ≤ C) (x : P) : E.map (EC.map x) = E.map x := by
…
```
Mentions: OAI.KadisonSimilarity.TracialExpectation

theorem OAI.KadisonSimilarity.TracialExpectation.eq_of_trace_tests line 91

Source documentation

Faithful trace pairings separate two elements of any star subalgebra.

theorem eq_of_trace_tests (B : StarSubalgebra ℂ P) (x y : P)
    (hx : x ∈ B) (hy : y ∈ B)
    (htest : ∀ c, c ∈ B → τ (c * x) = τ (c * y)) : x = y := by
…

theorem OAI.KadisonSimilarity.TracialExpectation.restricted_tower line 103
Source documentation
The expectation tower identity is only needed on a specified word subalgebra. This version applies when the base expectation of those words lands in a smaller algebra contained in the intermediate algebra; the whole base algebra need not be contained in that intermediate algebra.
```
theorem restricted_tower {C S B : StarSubalgebra ℂ P}
    (EC : TracialExpectation τ C) (hCS : C ≤ S) (hBA : B ≤ A) (hBC : B ≤ C)
    (hmap : ∀ x, x ∈ S → E.map x ∈ B) (x : P) (hx : x ∈ S) :
    E.map (EC.map x) = E.map x := by
…
```
Mentions: OAI.KadisonSimilarity.TracialExpectation

theorem OAI.KadisonSimilarity.TracialExpectation.free_compression line 114

Source documentation

Scalar freeness now gives the free-compression expectation formula for this actual expectation map.

theorem free_compression (hτ : τ 1 = 1)
    (htr : ∀ x y, τ (x * y) = τ (y * x))
    {D : StarSubalgebra ℂ P} (hfree : ScalarFree τ D A)
    {e b : P} (he : e ∈ D) (hb : b ∈ A) (hb0 : τ b = 0) :
    E.map (e * b * e) = (τ e) ^ 2 • b :=
…

Mentions: OAI.KadisonSimilarity.ScalarFree

theorem OAI.KadisonSimilarity.TracialCornerGeometry.expectation_base_projection line 130
Source documentation
Conditional expectation on algebra vectors is exactly orthogonal projection onto the actual closed base Hilbert space.
```
theorem expectation_base_projection (x : P) :
    (G.baseInclusion A).toContinuousLinearMap.adjoint (G.vector x) =
      G.baseVector A ⟨E.map x, E.range x⟩ := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.expectation_vector_norm_le line 144
Source documentation
Expectation is contractive for the tracial Hilbert norm.
```
theorem expectation_vector_norm_le (x : P) : ‖G.vector (E.map x)‖ ≤ ‖G.vector x‖ := by
…
```