FiniteBaseFreeHaar.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A free Haar unitary for the finite scalar matrix base

Finite dimensionality supplies the separability premise of the published independence input. Centering the base is an actual submodule, and testing against scalar multiples of one is exactly the required orthogonality.

theorem OAI.KadisonKastler.traceSeparable_of_separable line 21
Source documentation
Norm separability implies separability for the weaker trace norm.
```
theorem traceSeparable_of_separable (τ : FaithfulTracialState B)
    (X : Submodule ℂ B) [SeparableSpace X] : TraceSeparable τ (X : Set B) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.TraceSeparable
def OAI.KadisonKastler.centeredBase line 31
Source documentation
The centered linear subspace of a base star algebra.
```
def centeredBase (τ : FaithfulTracialState B) (A : StarSubalgebra ℂ B) :
    Submodule ℂ B := A.toSubmodule ⊓ LinearMap.ker τ.toLinearMap
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.mem_centeredBase line 35
theorem OAI.KadisonKastler.traceOrthogonal_bot line 38
theorem OAI.KadisonKastler.FiniteBaseIndependence.exists_freeHaar line 47
Source documentation
Popa's published finite-base independence theorem, applied with scalar base, produces the precise free-Haar moments for any finite dimensional subalgebra.
```
theorem FiniteBaseIndependence.exists_freeHaar
    (τ : FaithfulTracialState B) (h : FiniteBaseIndependence τ)
    (A : StarSubalgebra ℂ B) [FiniteDimensional ℂ A] :
    ∃ w : unitary B, FreeHaarMoments τ A w := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.FiniteBaseIndependence, OAI.KadisonKastler.FreeHaarMoments