PublishedIndependence.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Popa's finite-base independence input

Popa, Independence properties in subalgebras of ultraproduct II1 factors, J. Funct. Anal. 266 (2014), Theorem 0.1(b), Theorem 4.3 and its proof, printed pp. 20 and 24 (arXiv:1308.3982v3).

Theorem 4.3 explicitly permits both endpoint letters to be one. Its proof constructs the diffuse abelian algebra from a Haar unitary. We retain exactly that unitary and the mixed-moment identity, only for a finite base algebra. Testing the conditional expectation against base elements is its faithful-trace characterization. No controlled coordinate lift or scalar freeness of a conjugated matrix model is assumed here.

def OAI.KadisonKastler.TraceSeparable line 29
Source documentation
Separability for the tracial two-norm, rather than the operator norm.
```
def TraceSeparable (τ : FaithfulTracialState C) (S : Set C) : Prop :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
def OAI.KadisonKastler.TraceOrthogonal line 35
Source documentation
Orthogonality to the base algebra, equivalently zero conditional expectation onto it.
```
def TraceOrthogonal (τ : FaithfulTracialState C) (D : StarSubalgebra ℂ C) (x : C) : Prop :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
def OAI.KadisonKastler.HaarEndpointIndependence line 40
Source documentation
Popa's precise mixed word, with the initial and final letters optional. The r + 1 nonzero Haar powers are interleaved with the r letters in l.
```
def HaarEndpointIndependence (τ : FaithfulTracialState C)
    (D : StarSubalgebra ℂ C) (X : Submodule ℂ C) (w : unitary C) : Prop :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
def OAI.KadisonKastler.FiniteBaseIndependence line 50
Source documentation
The finite-base specialization of the published independence theorem. Its domain remains a tracial ultraproduct in the input declarations below.
```
def FiniteBaseIndependence (τ : FaithfulTracialState C) : Prop :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
def OAI.KadisonKastler.PublishedPopaFiniteBaseIndependence line 62
Source documentation
The published independence input for the two ultraproducts actually used in the controlled-lift construction: constant II1 factors and the increasing finite-matrix model.
```
def PublishedPopaFiniteBaseIndependence : Prop :=
…
```