FiniteBaseConjugation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Applying second-stage independence to the actual finite base projection

theorem OAI.KadisonKastler.traceBaseProjection_finiteBaseExpectation line 14
theorem OAI.KadisonKastler.freeHaarMoments_of_position_independence line 22
Source documentation
The exact test space used by the second finite-base independence application yields scalar freeness relative to the prescribed algebra.
```
theorem freeHaarMoments_of_position_independence
    {τ : FaithfulTracialState B} {D A : StarSubalgebra ℂ B}
    [FiniteDimensional ℂ D] (hDA : D ≤ A) {s w : unitary B}
    (hs : FreeHaarMoments τ D s)
    (hw : ∀ d ∈ D, Commute (w : B) d)
    (hind : HaarEndpointIndependence τ D (positionTestSpace τ D A (s : B)) w) :
    FreeHaarMoments τ A (w * s * star w) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.HaarEndpointIndependence, OAI.KadisonKastler.positionTestSpace

theorem OAI.KadisonKastler.FiniteBaseIndependence.exists_conjugated_freeHaar line 40

Source documentation

Popa's finite-base independence, together with the proved scalar conversion, moves a model Haar unitary into free position relative to A.

theorem FiniteBaseIndependence.exists_conjugated_freeHaar
    {τ : FaithfulTracialState B} (h : FiniteBaseIndependence τ)
    (D A : StarSubalgebra ℂ B) [FiniteDimensional ℂ D]
    (hDA : D ≤ A) (hA : TraceSeparable τ (A : Set B))
    (s : unitary B) (hs : FreeHaarMoments τ D s) :
    ∃ w : unitary B, (∀ d ∈ D, Commute (w : B) d) ∧
      FreeHaarMoments τ A (w * s * star w) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.FiniteBaseIndependence, OAI.KadisonKastler.TraceSeparable, OAI.KadisonKastler.FreeHaarMoments